move lemma-just!=nothing to FinMap and use it there
[~helmut/bidiragda.git] / Bidir.agda
index 99a3fd0..3875394 100644 (file)
@@ -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