Step * of Lemma PiDataVal_wf

PiDataVal() ∈ Type
BY
Unfold `PiDataVal` THEN Auto }


Latex:


Latex:
PiDataVal()  \mmember{}  Type


By


Latex:
Unfold  `PiDataVal`  0  THEN  Auto




Home Index