diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2013-01-09 23:24:58 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2013-01-09 23:24:58 +0100 |
| commit | ec47ee14b9154410b7c72fb067671ea79fd71523 (patch) | |
| tree | f143685dea8d4db96b7a9a27b81a8323b598049e | |
| parent | 55d4808670b0de9ecc117f81eb61b33b70d63536 (diff) | |
| download | bidiragda-ec47ee14b9154410b7c72fb067671ea79fd71523.tar.gz | |
simplify lemma-lookupM-checkInsert using case-split
| -rw-r--r-- | CheckInsert.agda | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index ad0bb1a..7e3f3aa 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -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 |