---

Step * of Lemma l_all_assert_iff_reduce

∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List].  uiff((∀x∈L.↑P[x]);↑reduce(λx,b. (P[x] ∧b b);tt;L))
BY
{ (InductionOnList THEN Reduce 0) }

1
1. A : Type
2. P : A ⟶ 𝔹
⊢ uiff((∀x∈[].↑P[x]);True)

2
1. A : Type
2. P : A ⟶ 𝔹
3. u : A@i
4. v : A List@i
5. uiff((∀x∈v.↑P[x]);↑reduce(λx,b. (P[x] ∧b b);tt;v))@i
⊢ uiff((∀x∈[u / v].↑P[x]);↑(P[u] ∧b reduce(λx,b. (P[x] ∧b b);tt;v)))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].    uiff((\mforall{}x\mmember{}L.\muparrow{}P[x]);\muparrow{}reduce(\mlambda{}x,b.  (P[x]  \mwedge{}\msubb{}  b);tt;L))


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index