Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_d0012009c84eec7f5a959d2efcafb6038b43c2e7681a7479cff0214b7d857f00 with
λ x3 x4 : ι → ι → ι . In x2 (x4 x0 x1).
Apply unknownprop_bb7319fda7123d5f775b6b29aaea60dee8b8450dbda3fb13de42ee7deaa111d5 with
UPair x0 x1,
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_062c64c10c58e9562a87a79165ec64b8525d3f91b15ae8561687c786947b4cb0 with x0, x1.