Step
*
of Lemma
per-void_wf
per-void() ∈ Type
BY
{ (Unfold `per-void` 0 THEN PerEqCD THEN Auto) }
Latex:
Latex:
per-void()  \mmember{}  Type
By
Latex:
(Unfold  `per-void`  0  THEN  PerEqCD  THEN  Auto)
Home
Index