simplify lemma-lookupM-checkInsert using case-split
authorHelmut Grohne <helmut@subdivi.de>
Wed, 9 Jan 2013 22:24:58 +0000 (23:24 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Wed, 9 Jan 2013 22:24:58 +0000 (23:24 +0100)
CheckInsert.agda

index ad0bb1a..7e3f3aa 100644 (file)
@@ -82,10 +82,5 @@ lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' | no
     ≡⟨ pl ⟩
   just x ∎
 lemma-lookupM-checkInsert i j x y h h' pl ph' | just z | pl' with deq y z
-lemma-lookupM-checkInsert i j x y h h' pl ph' | just .y | pl' | yes refl = begin
-  lookupM i h'
-    ≡⟨ cong (lookupM i) (just-injective (sym ph')) ⟩
-  lookupM i h
-    ≡⟨ pl ⟩
-  just x ∎
+lemma-lookupM-checkInsert i j x y h .h pl refl | just .y | pl' | yes refl = pl
 lemma-lookupM-checkInsert i j x y h h' pl () | just z | pl' | no p