Step
*
of Lemma
dl-Spec_wf
dl-Spec() ∈ MutualRectypeSpec
BY
{ (Unfold `mrec_spec` 0 THEN ProveWfLemma) }
Latex:
Latex:
dl-Spec()  \mmember{}  MutualRectypeSpec
By
Latex:
(Unfold  `mrec\_spec`  0  THEN  ProveWfLemma)
Home
Index