---

Step * of Lemma list-set-type2

∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ ℙ].  L ∈ {x:T| P[x]}  List supposing (∀x∈L.P[x])
BY
{ (((Auto THEN (InstLemma `list-set-type` [⌜T⌝; ⌜L⌝])⋅) THENA Auto)
   THEN (DoSubsume THEN Auto)
   THEN SubtypeReasoning
   THEN Auto
   THEN Thin (-4)⋅
   THEN RWO "l_all_iff" (-4)
   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:
(((Auto  THEN  (InstLemma  `list-set-type`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{})  THENA  Auto)
  THEN  (DoSubsume  THEN  Auto)
  THEN  SubtypeReasoning
  THEN  Auto
  THEN  Thin  (-4)\mcdot{}
  THEN  RWO  "l\_all\_iff"  (-4)
  THEN  Auto)

---

Home Index