---

Step * of Lemma property-from-l_member

∀[T:Type]. ∀x:T. ∀[P:T ⟶ ℙ]. ((∀x:T. SqStable(P[x])) ⇒ (∀d:{i:T| P[i]}  List. ((x ∈ d) ⇒ P[x])))
BY
{ (InstLemma `l_member_settype` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN ParallelOp -2
   THEN ParallelLast) }

1
1. [T] : Type
2. x : T@i
3. [P] : T ⟶ ℙ
4. ∀[d:{i:T| P[i]}  List]. x ∈ {x:T| P[x]}  supposing (x ∈ d)
5. ∀x:T. SqStable(P[x])@i
6. d : {i:T| P[i]}  List@i
7. (x ∈ d)@i
8. x ∈ {x:T| P[x]} 
⊢ P[x]

---

Latex:

---

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


By

---

Latex:
(InstLemma  `l\_member\_settype`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  ParallelLast)

---

Home Index