---

Step * of Lemma list_set_type

∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ ℙ].  L ∈ {x:T| P[x]}  List supposing (∀x∈L.P[x])
BY
{ (((InductionOnList THEN Auto THEN (RWO "l_all_cons" (-1))) THENA Auto) THEN Try (BackThruSomeHyp) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    L  \mmember{}  \{x:T|  P[x]\}    List  supposing  (\mforall{}x\mmember{}L.P[x])


By

---

Latex:
(((InductionOnList  THEN  Auto  THEN  (RWO  "l\_all\_cons"  (-1)))  THENA  Auto)
  THEN  Try  (BackThruSomeHyp)
  THEN  Auto)

---

Home Index