From 7dcad0cd17c75867c2ce10ac72c9863fb3ed2e94 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 25 Oct 2012 12:53:19 +0200 Subject: rename lemma-from-just to just-injective We already have suc-injective and \::-injective. Consistency! --- CheckInsert.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'CheckInsert.agda') 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 ∎ -- cgit v1.2.3