From 7c3e2c61e55aa876f88fbd34c94ccfb0a8c715d4 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Thu, 19 Apr 2012 11:52:27 +0200
Subject: move lemma-just!=nothing to FinMap and use it there

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

(limited to 'Bidir.agda')

diff --git a/Bidir.agda b/Bidir.agda
index 99a3fd0..3875394 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -66,9 +66,6 @@ lemma-checkInsert-wrong eq i x m x' d refl | .(just x') with eq x x'
 lemma-checkInsert-wrong eq i x m x' d refl | .(just x') | yes q = contradiction q d
 lemma-checkInsert-wrong eq i x m x' d refl | .(just x') | no ¬q = refl
 
-lemma-just≢nothing : {A Whatever : Set} {a : A} → _≡_ {_} {Maybe A} (just a) nothing → Whatever
-lemma-just≢nothing ()
-
 record checkInsertEqualProof {A : Set} {n : ℕ} (eq : EqInst A) (i : Fin n) (x : A) (m : FinMapMaybe n A) (e : Maybe (FinMapMaybe n A)) : Set where
   field
      same : lookupM i m ≡ just x → just m ≡ e
-- 
cgit v1.2.3