---

Step * of Lemma reduce-bool-bfalse

∀T:Type. ∀f:T ─→ 𝔹 ─→ 𝔹. ∀L:T List.  (reduce(λx,b. (b ∧b f[x;b]);ff;L) ~ ff)
BY
{ ((UnivCD THENA Auto) THEN ListInd (-1) THEN Reduce 0 THEN Auto THEN HypSubst' (-1) 0 THEN Auto) }

---

Latex:


\mforall{}T:Type.  \mforall{}f:T  {}\mrightarrow{}  \mBbbB{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.    (reduce(\mlambda{}x,b.  (b  \mwedge{}\msubb{}  f[x;b]);ff;L)  \msim{}  ff)


By

((UnivCD  THENA  Auto)  THEN  ListInd  (-1)  THEN  Reduce  0  THEN  Auto  THEN  HypSubst'  (-1)  0  THEN  Auto)

---

Home Index