express VecBFF via PartialVecBFF

1 files changed, 2 insertions, 3 deletions

diff --git a/FreeTheorems.agda b/FreeTheorems.agda
index aacb95a..c22a68d 100644
--- a/FreeTheorems.agda
+++ b/FreeTheorems.agda
@@ -11,6 +11,8 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming
 open import Relation.Binary using (Setoid)
 open Injection using (to)
 
+open import Generic using (≡-to-Π)
+
 module ListList where
   get-type : Set₁
   get-type = {A : Set} → List A → List A
@@ -37,8 +39,5 @@ module PartialVecVec where
 
   open VecVec using () renaming (free-theorem-type to VecVec-free-theorem-type)
 
-  ≡-to-Π : {A B : Set} → (A → B) → EqSetoid A ⟶ EqSetoid B
-  ≡-to-Π f = record { _⟨$⟩_ = f; cong = cong f }
-
   VecVec-free-theorem : VecVec-free-theorem-type
   VecVec-free-theorem {getlen} get = free-theorem Function.Injection.id (≡-to-Π getlen) get