---

Step * 1 1 of Lemma l_member_type


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)
7. P x
⊢ P x
BY
{ Trivial }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x  :  T
3.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
4.  d  :  \{i:T|  P  i\}    List
5.  \mforall{}y:T.  Dec(P  y)
6.  (x  \mmember{}  d)
7.  P  x
\mvdash{}  P  x


By

---

Latex:
Trivial

---

Home Index