---

Step * of Lemma member_singleton

∀[T:Type]. ∀a,x:T.  ((x ∈ [a]) ⇐⇒ x = a ∈ T)
BY
{ ((((Unfold `l_member` 0 THEN Reduce 0) THEN Auto) THEN ExRepD) THEN Reduce 0) }

1
1. T : Type
2. a : T
3. x : T
4. i : ℕ
5. i < 1
6. x = [a][i] ∈ T
⊢ x = a ∈ T

2
1. [T] : Type
2. a : T
3. x : T
4. x = a ∈ T
⊢ ∃i:ℕ. (i < 1 c∧ (x = [a][i] ∈ T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}a,x:T.    ((x  \mmember{}  [a])  \mLeftarrow{}{}\mRightarrow{}  x  =  a)


By

---

Latex:
((((Unfold  `l\_member`  0  THEN  Reduce  0)  THEN  Auto)  THEN  ExRepD)  THEN  Reduce  0)

---

Home Index