Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι → ο be given.
Assume H1: x5 x0.
Assume H2: x5 x1.
Assume H3: x5 x2.
Assume H4: x5 x3.
Apply binunionE with
SetAdjoin (UPair x0 x1) x2,
Sing x3,
x4,
x5 x4 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_81da4a4b6c1b1603a521d080942fe6e652095cdddea7d0d491d4c44dcea723fa with
x0,
x1,
x2,
x4,
x5 leaving 4 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply SingE with
x3,
x4,
λ x6 x7 . x5 x7 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.