diff options
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 ∎ |