Step 
*
 of Lemma 
ses-info_wf
∀[s:SES]. (Info ∈ Type)
BY
 
{ (ProveWfLemma THEN D -1 THEN Auto) }
 
Latex: 
Latex:
\mforall{}[s:SES].  (Info  \mmember{}  Type)
 By 
Latex:
(ProveWfLemma  THEN  D  -1  THEN  Auto)
Home
Index