Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_5d43e074a46031aba9b972e1346a32eab5bc6d7f8cd872222d3a15fe3889dd90 with
λ x3 x4 : ι → ι → ο . x4 x0 x2 ⟶ x4 x1 x2 ⟶ x4 (binunion x0 x1) x2.
Assume H0:
∀ x3 . In x3 x0 ⟶ In x3 x2.
Assume H1:
∀ x3 . In x3 x1 ⟶ In x3 x2.
Let x3 of type ι be given.
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with
x0,
x1,
x3,
In x3 x2 leaving 3 subgoals.
The subproof is completed by applying H2.
Apply H0 with
x3.
The subproof is completed by applying H3.
Apply H1 with
x3.
The subproof is completed by applying H3.