---

Step * of Lemma l_member_settype

∀[T:Type]. ∀[x:T]. ∀[P:T ⟶ ℙ]. ∀[d:{i:T| P[i]}  List].  x ∈ {x:T| P[x]}  supposing (x ∈ d)
BY
{ ((Unfold `so_apply` 0 THEN Auto) THEN RepeatFor 2 (D -1) THEN (Assert ⌜d[i] ∈ {i:T| P i} ⌝⋅ THEN Auto)⋅) }

---

Latex:

---

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


By

---

Latex:
((Unfold  `so\_apply`  0  THEN  Auto)  THEN  RepeatFor  2  (D  -1)  THEN  (Assert  \mkleeneopen{}d[i]  \mmember{}  \{i:T|  P  i\}  \mkleeneclose{}\mcdot{}  THEN  Aut\000Co)\mcdot{})

---

Home Index