diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-16 10:57:31 +0200 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-16 10:57:31 +0200 |
| commit | 71c4040262bd1c0ac5962425ee4b3bb3b51cc93b (patch) | |
| tree | 796d7fa99a2f20bdbac3e4cfcb400083d733dc93 /Precond.agda | |
| parent | d2548922c7abb20fee5633be6e654430517555af (diff) | |
| download | bidiragda-71c4040262bd1c0ac5962425ee4b3bb3b51cc93b.tar.gz | |
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.
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 2 |
1 files changed, 1 insertions, 1 deletions
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 ∎ |