From 0a34343e2cd20be26411af267a57b54fd300cf38 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Sun, 22 Jan 2012 22:36:16 +0100
Subject: formulate lemma-2

---
 Bidir.agda | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Bidir.agda b/Bidir.agda
index 736b910..e77de94 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -80,6 +80,9 @@ lemma-1 eq f (i ∷ is′) | just m | .m | refl | just x with eq (f i) x
 lemma-1 eq f (i ∷ is′) | just m | .m | refl | just .(f i) | yes refl = cong just (lemma-insert-same m i {!!})
 lemma-1 eq f (i ∷ is′) | just m | .m | refl | just x | no ¬p = {!!}
 
+lemma-2 : {τ : Set} {n : ℕ} → (eq : (x y : τ) → Dec (x ≡ y)) → (is : List (Fin n)) → (v : List τ) → (h : FinMapMaybe n τ) → just h ≡ assoc eq is v → map (flip lookup h) is ≡ map just v
+lemma-2 eq is v h p = {!!}
+
 idrange : (n : ℕ) → List (Fin n)
 idrange n = toList (tabulate id)
 
-- 
cgit v1.2.3