From 925dbb2dac110d46130715464d7877b5b660ced0 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 9 Feb 2012 16:04:32 +0100 Subject: avoid a sym in lemma-union-restrict --- FinMap.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'FinMap.agda') diff --git a/FinMap.agda b/FinMap.agda index 376adff..03a304b 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -122,11 +122,11 @@ lemma-union-restrict f is = begin lookup j (fromFunc f) ≡⟨ lookup∘tabulate f j ⟩ f j ∎ - lemma-inner f (i ∷ is) j with i ≟ j + lemma-inner f (i ∷ is) j with j ≟ i lemma-inner f (.j ∷ is) j | yes refl = cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-insert j (f j) (restrict f is)) - lemma-inner f (i ∷ is) j | no i≢j = begin + lemma-inner f (i ∷ is) j | no j≢i = begin maybe′ id (lookup j (fromFunc f)) (lookupM j (insert i (f i) (restrict f is))) - ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (sym (lemma-lookupM-insert-other j i (f i) (restrict f is) (i≢j ∘ sym) )) ⟩ + ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (sym (lemma-lookupM-insert-other j i (f i) (restrict f is) j≢i)) ⟩ maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)) ≡⟨ lemma-inner f is j ⟩ f j ∎ -- cgit v1.2.3