---

Step * of Lemma l_member_in_subtype2

∀[T:Type]. ∀x:T. ∀[P:T ⟶ ℙ]. ∀d:{i:T| P[i]}  List. ((x ∈ d) ⇒ (x ∈ d))
BY
{ (Unfold `so_apply` 0
   THEN Auto
   THEN RepeatFor 2 (D -1)
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;3]
   THEN D (-2)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `so\_apply`  0
  THEN  Auto
  THEN  RepeatFor  2  (D  -1)
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;3]
  THEN  D  (-2)
  THEN  Auto)

---

Home Index