---

Step * of Lemma fset-singletons-equal

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T].  uiff({x} = {y} ∈ fset(T);x = y ∈ T)
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. y : T
5. {x} = {y} ∈ fset(T)
⊢ x = y ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x,y:T].    uiff(\{x\}  =  \{y\};x  =  y)


By

---

Latex:
Auto

---

Home Index