From d2548922c7abb20fee5633be6e654430517555af Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Wed, 15 Oct 2014 10:35:43 +0200 Subject: remove lemma-just≢nothing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Special case of contradiction. --- CheckInsert.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'CheckInsert.agda') diff --git a/CheckInsert.agda b/CheckInsert.agda index 16bcc8e..9dc8a60 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -67,7 +67,7 @@ lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (x y : Carrier) → lemma-lookupM-checkInsert i j x y h h' pl ph' with checkInsert j y h | insertionresult j y h lemma-lookupM-checkInsert i j x y h .h pl refl | ._ | same _ _ _ = pl lemma-lookupM-checkInsert i j x y h h' pl ph' | ._ | new _ with i ≟ j -lemma-lookupM-checkInsert i .i x y h h' pl ph' | ._ | new pl' | yes refl = lemma-just≢nothing pl pl' +lemma-lookupM-checkInsert i .i x y h h' pl ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ()) lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no i≢j = begin lookupM i (insert j y h) ≡⟨ sym (lemma-lookupM-insert-other i j y h i≢j) ⟩ -- cgit v1.2.3