---

Step * of Lemma l_member-set2

∀[T:Type]. ∀[P:T ⟶ ℙ].  ∀L:{x:T| P[x]}  List. ∀x:T.  ((x ∈ L) ⇒ (x ∈ {x:T| P[x]} ))
BY
{ (InductionOnList
   THEN (UnivCD THENA Auto)
   THEN (RWO "nil_member cons_member" (-1) THENA Auto)
   THEN (Trivial ⋅ ORELSE (All DSet THEN D (-1) THEN Auto THEN MemTypeCD THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(InductionOnList
  THEN  (UnivCD  THENA  Auto)
  THEN  (RWO  "nil\_member  cons\_member"  (-1)  THENA  Auto)
  THEN  (Trivial  \mcdot{}  ORELSE  (All  DSet  THEN  D  (-1)  THEN  Auto  THEN  MemTypeCD  THEN  Auto)))

---

Home Index