---

Step * of Lemma list-set-type-member

∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. SqStable(P[x])) ⇒ (∀L:{x:T| P[x]}  List. ∀x:T.  {(x ∈ L) ⇒ P[x]}))
BY
{ ((Unfold `guard` 0 THEN Auto)
   THEN RepeatFor 2 (D -1)
   THEN HypSubst' -1 0
   THEN Auto
   THEN GenConclAtAddr [2]
   THEN Auto
   THEN D (-2)
   THEN Unhide
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Unfold  `guard`  0  THEN  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  HypSubst'  -1  0
  THEN  Auto
  THEN  GenConclAtAddr  [2]
  THEN  Auto
  THEN  D  (-2)
  THEN  Unhide
  THEN  Auto)

---

Home Index