Step * of Lemma dl-Spec_wf

dl-Spec() ∈ MutualRectypeSpec
BY
(Unfold `mrec_spec` THEN ProveWfLemma) }


Latex:


Latex:
dl-Spec()  \mmember{}  MutualRectypeSpec


By


Latex:
(Unfold  `mrec\_spec`  0  THEN  ProveWfLemma)




Home Index