---

Step * of Lemma list_all_wf

∀[T:Type]. ∀[l:T List]. ∀[P:T ⟶ ℙ].  (list_all(x.P[x];l) ∈ ℙ)
BY
{ ((((UnivCD THENA Auto) THEN Unfold `list_all` 0) THEN BackThruLemma `reduce_wf`) THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    (list\_all(x.P[x];l)  \mmember{}  \mBbbP{})


By

---

Latex:
((((UnivCD  THENA  Auto)  THEN  Unfold  `list\_all`  0)  THEN  BackThruLemma  `reduce\_wf`)
  THEN  Try  (Complete  (Auto))
  )

---

Home Index