Let x0 of type ι be given.
Assume H1: 1 ∈ x0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H4: x3 ∈ x1.
Let x4 of type ι be given.
Assume H5: x4 ∈ x2.
Apply set_ext with
x3,
x4 leaving 2 subgoals.
Apply unknownprop_63f7c049c04cf6dd8522f23c2ad60bce02e050a2c7835473668a67ed6b19a82c with
x0,
x1,
x2,
x3,
x4 leaving 7 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Apply unknownprop_63f7c049c04cf6dd8522f23c2ad60bce02e050a2c7835473668a67ed6b19a82c with
x0,
x2,
x1,
x4,
x3 leaving 7 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
Let x5 of type ι → ι → ο be given.
The subproof is completed by applying H6 with λ x6 x7 . x5 x7 x6.