formulate theorem-2

1 files changed, 3 insertions, 0 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 332cc55..23381d0 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -151,3 +151,6 @@ theorem-1 get eq s = begin
   just (map (denumerate s) (enumerate s))
     ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩
   just s ∎
+
+theorem-2 : (get : {α : Set} → List α → List α) → {τ : Set} → (eq : EqInst τ) → (v s u : List τ) → bff get eq s v ≡ just u → get u ≡ v
+theorem-2 get eq v s u p = {!!}