diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-02-09 16:04:32 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-02-09 16:04:32 +0100 |
| commit | 925dbb2dac110d46130715464d7877b5b660ced0 (patch) | |
| tree | d5d663e78adebaecb89c3eabfb332a4ab4d1fdbe | |
| parent | 7673d048da79e050474c4396bcbd57f2632bd939 (diff) | |
| download | bidiragda-925dbb2dac110d46130715464d7877b5b660ced0.tar.gz | |
avoid a sym in lemma-union-restrict
| -rw-r--r-- | FinMap.agda | 6 |
1 files changed, 3 insertions, 3 deletions
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 ∎ |