---

Step * of Lemma bunion-value-type

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  AutoSplit)

---

Home Index