From 16d6ec0aa1f8599a4445ea6994d6f0fb5e5c25d4 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Mon, 23 Jan 2012 19:51:55 +0100
Subject: base case of lemma-2

---
 Bidir.agda | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Bidir.agda b/Bidir.agda
index 07193c7..51b24b1 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -101,7 +101,10 @@ lemma-1 eq f (i ∷ is′) = begin
      where open Relation.Binary.PropositionalEquality.≡-Reasoning
 
 lemma-2 : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (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 = {!!}
+lemma-2 eq []       []       h p = refl
+lemma-2 eq []       (x ∷ xs) h ()
+lemma-2 eq (x ∷ xs) []       h ()
+lemma-2 eq (i ∷ is) (x ∷ xs) h p = {!!}
 
 idrange : (n : ℕ) → List (Fin n)
 idrange n = toList (tabulate id)
-- 
cgit v1.2.3