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