From 71c4040262bd1c0ac5962425ee4b3bb3b51cc93b Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 16 Oct 2014 10:57:31 +0200 Subject: sym result of lemma-lookupM-{i,checkI}nsert-other Typically we have the complex term on the LHS and the simplified term on the RHS. These lemmata did it otherwise and by symming them, we save two syms. --- Precond.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Precond.agda') diff --git a/Precond.agda b/Precond.agda index 85c955c..8d2eab2 100644 --- a/Precond.agda +++ b/Precond.agda @@ -100,7 +100,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-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' h ph) ⟩ + ≡⟨ 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