Step
*
of Lemma
Id_wf
Id ∈ Type
BY
{ (Unfold `Id` 0 THEN Auto) }
Latex:
Latex:
Id \mmember{} Type
By
Latex:
(Unfold `Id` 0 THEN Auto)
Home
Index