Step
*
of Lemma
labeled-graph_wf
∀[T:Type]. (LabeledGraph(T) ∈ Type)
BY
{ (ProveWfLemma THEN BLemma `dep-isect-wf`  THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type].  (LabeledGraph(T)  \mmember{}  Type)
By
Latex:
(ProveWfLemma  THEN  BLemma  `dep-isect-wf`    THEN  Auto)
Home
Index