Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply UnionI with
94f9e.. 48ef8.. (λ x3 . prim0 (aa8d2.. x3 x0)),
x1,
prim0 (aa8d2.. x2 x0) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with
48ef8..,
λ x3 . prim0 (aa8d2.. x3 x0),
x2.
Apply unknownprop_b67f6d586fb9d8883c38540f89ba210beeb3fabc8048f066af6580d3cbff51ec with
x2.
The subproof is completed by applying H0.