Step
*
of Lemma
norm-components_wf
∀[M:Type ─→ Type]. norm-components ∈ id-fun(component(P.M[P]) List) supposing M[Top]
BY
{ (ProveWfLemma THEN BLemma `component-has-value` THEN Auto) }
Latex:
Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  norm-components  \mmember{}  id-fun(component(P.M[P])  List)  supposing  M[Top]
By
Latex:
(ProveWfLemma  THEN  BLemma  `component-has-value`  THEN  Auto)
Home
Index