Step
*
of Lemma
decision_wf
Decision ∈ Type
BY
{ (Unfold `decision` 0 THEN Auto{1,3}-1) }
Latex:
Latex:
Decision  \mmember{}  Type
By
Latex:
(Unfold  `decision`  0  THEN  Auto\{1,3\}-1)
Home
Index