---

Step * of Lemma equal-value-type

∀[T:Type]. ∀[x,y:T].  value-type(x = y ∈ T)
BY
{ ValueTypeAuto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x,y:T].    value-type(x  =  y)


By

---

Latex:
ValueTypeAuto

---

Home Index