---

Step * of Lemma uand_wf

∀[A,B:Type].  (uand(A;B) ∈ Type)
BY
{ (ProveWfLemma THEN CanonicalAuto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (uand(A;B)  \mmember{}  Type)


By

---

Latex:
(ProveWfLemma  THEN  CanonicalAuto)

---

Home Index