Step
*
of Lemma
rng_lsum_when_swap
∀r:Rng. ∀A:Type. ∀f:A ⟶ |r|. ∀b:𝔹. ∀as:A List.
((Σ{A,r} x ∈ as. (when b. f[x])) = (when b. (Σ{A,r} x ∈ as. f[x])) ∈ |r|)
BY
{ (InductionOnList⋅ THEN Reduce 0 THEN Auto) }
Latex:
Latex:
\mforall{}r:Rng. \mforall{}A:Type. \mforall{}f:A {}\mrightarrow{} |r|. \mforall{}b:\mBbbB{}. \mforall{}as:A List.
((\mSigma{}\{A,r\} x \mmember{} as. (when b. f[x])) = (when b. (\mSigma{}\{A,r\} x \mmember{} as. f[x])))
By
Latex:
(InductionOnList\mcdot{} THEN Reduce 0 THEN Auto)
Home
Index