---

Step * 1 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)
⊢ P x
BY
{ (((InstHyp [⌜x⌝] (-2))⋅ THENA Auto) THEN D -1) }

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)
7. P x
⊢ P x

2
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

---

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


By

---

Latex:
(((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-2))\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index