diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-10-25 12:53:19 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-10-25 12:53:19 +0200 |
| commit | 7dcad0cd17c75867c2ce10ac72c9863fb3ed2e94 (patch) | |
| tree | a0c6cca57eca277ff0d647d6d9fdab3e97146a3d /CheckInsert.agda | |
| parent | f622e4cfa50a46761a7344c9ad980f983f5f42ec (diff) | |
| download | bidiragda-7dcad0cd17c75867c2ce10ac72c9863fb3ed2e94.tar.gz | |
rename lemma-from-just to just-injective
We already have suc-injective and \::-injective. Consistency!
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index 01f1302..6b5473a 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -84,7 +84,7 @@ lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' | no 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) (lemma-from-just (sym ph')) ⟩ + ≡⟨ cong (lookupM i) (just-injective (sym ph')) ⟩ lookupM i h ≡⟨ pl ⟩ just x ∎ |