Step
*
of Lemma
union-wf
∀[A,B:Type].  (A + B ∈ Type)
BY
{ Auto }
Latex:
Latex:
\mforall{}[A,B:Type].    (A  +  B  \mmember{}  Type)
By
Latex:
Auto
Home
Index