---

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