Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_99c6830b7507eb1c538c7366f637e956be6dad337531dd2702ca6ba6923a9849 with
UPair x0 x1,
x2,
or (In x2 x0) (In x2 x1) leaving 2 subgoals.
Apply unknownprop_d0012009c84eec7f5a959d2efcafb6038b43c2e7681a7479cff0214b7d857f00 with
λ x3 x4 : ι → ι → ι . In x2 (x3 x0 x1).
The subproof is completed by applying H0.
Let x3 of type ι be given.
Apply unknownprop_75ddf832b1631756e4bbf96a65e15fca654982aa51c8799a97b68da7b8a2da12 with
x3,
x0,
x1,
or (In x2 x0) (In x2 x1) leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: x3 = x0.
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
In x2 x0,
In x2 x1.
Apply H3 with
λ x4 x5 . In x2 x4.
The subproof is completed by applying H1.
Assume H3: x3 = x1.
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
In x2 x0,
In x2 x1.
Apply H3 with
λ x4 x5 . In x2 x4.
The subproof is completed by applying H1.