---

Step * 1 2 of Lemma l_member_type2


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
{ (RepUR ``l_member`` -2 THEN SplitAndHyps) }

1
1. [T] : Type
2. x : T
3. [P] : T ⟶ ℙ
4. d : {i:T| P i}  List
5. ∀y:T. Dec(P y)
6. ∃i:ℕ. (i < ||d|| c∧ (x = d[i] ∈ T))
7. ¬(P x)
⊢ P x

---

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.  \mneg{}(P  x)
\mvdash{}  P  x


By

---

Latex:
(RepUR  ``l\_member``  -2  THEN  SplitAndHyps)

---

Home Index