---

Step * of Lemma bunion-valueall-type

∀[A,B:Type].  (valueall-type(A ⋃ B)) supposing (valueall-type(B) and valueall-type(A))
BY
{ (Auto THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (valueall-type(A  \mcup{}  B))  supposing  (valueall-type(B)  and  valueall-type(A))


By

---

Latex:
(Auto  THEN  AutoSplit)

---

Home Index