Step
*
of Lemma
equal-wf
∀[x,y:Base]. ∀[T:Type].  (x = y ∈ T ∈ Type)
BY
{ Auto }
Latex:
Latex:
\mforall{}[x,y:Base].  \mforall{}[T:Type].    (x  =  y  \mmember{}  Type)
By
Latex:
Auto
Home
Index