---

Step * of Lemma l_member_set2

∀[T:Type]. ∀[P:T ⟶ ℙ].  ∀L:{x:T| P[x]}  List. ∀x:T.  ((x ∈ L) ⇒ (x ∈ L))
BY
{ ((UnivCD THENA Auto)
   THEN (RepeatFor 2 (D (-1))
         THEN StrongHypSubst (-1) 0
         THEN Try (Complete (Auto))
         THEN MoveToConcl (-1)
         THEN GenConclAtAddr [1;3]
         THEN D -2
         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{}  L))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RepeatFor  2  (D  (-1))
              THEN  StrongHypSubst  (-1)  0
              THEN  Try  (Complete  (Auto))
              THEN  MoveToConcl  (-1)
              THEN  GenConclAtAddr  [1;3]
              THEN  D  -2
              THEN  Auto)\mcdot{}
  )

---

Home Index