Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with
x2,
famunion x0 (λ x4 . x1 x4) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_4d9a081a15fdc79c67eee9fe67650a775bc97737c16f9cc2a1a6fdd7a2cc8108 with
x0,
x1,
x3,
x2 leaving 2 subgoals.
Apply unknownprop_75b5762e65badae8f9531d40fddd332ff95b59f608d93c7a55f19f4fa5ef37d5 with
x3,
x0.
The subproof is completed by applying H1.
Apply unknownprop_75b5762e65badae8f9531d40fddd332ff95b59f608d93c7a55f19f4fa5ef37d5 with
x2,
x1 x3.
The subproof is completed by applying H2.