---

Step * of Lemma l_member_type2

∀[T:Type]. ∀x:T. ∀[P:T ⟶ ℙ]. ∀d:{i:T| P[i]}  List. ((∀y:T. Dec(P[y])) ⇒ (x ∈ d) ⇒ P[x])
BY
{ (Unfold `so_apply` 0 THEN Auto) }

1
1. [T] : Type
2. x : T
3. [P] : T ⟶ ℙ
4. d : {i:T| P i}  List
5. ∀y:T. Dec(P y)
6. (x ∈ d)
⊢ P x

---

Latex:

---

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


By

---

Latex:
(Unfold  `so\_apply`  0  THEN  Auto)

---

Home Index