From d42ffc9d24adb2b416ff73708ae64c1d4ca50c30 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 10 Jan 2013 11:09:38 +0100 Subject: reduce a precondition of lemma-checkInsert-lookupM Now it looks a lot more like lemma-lookupM-insert-other, so rename it to lemma-lookupM-checkInsert-other. --- Bidir.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Bidir.agda') diff --git a/Bidir.agda b/Bidir.agda index 901e2d1..3dbdbdd 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -62,7 +62,7 @@ lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is with assoc is' x lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h () i∉is | nothing | [ ph' ] lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is | just h' | [ ph' ] = begin lookupM i h - ≡⟨ sym (lemma-checkInsert-lookupM i i' (i∉is ∘ here) x' (lookupVec i h) h' h refl ph) ⟩ + ≡⟨ sym (lemma-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' h ph) ⟩ lookupM i h' ≡⟨ lemma-∉-lookupM-assoc i is' xs' h' ph' (i∉is ∘ there) ⟩ nothing ∎ -- cgit v1.2.3