---

Step * of Lemma l_member_type

∀[T:Type]. ∀x:T. ∀[P:T ⟶ ℙ]. ∀d:{i:T| P i}  List. ((∀y:T. Dec(P y)) ⇒ (x ∈ d) ⇒ (P x))
BY
{ 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:
Auto

---

Home Index