Let x0 of type ι be given.
Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with
x0,
0,
x0 = 0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι → ι be given.
Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with
x0,
0,
x1,
x0 = 0 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3:
∀ x2 . In x2 0 ⟶ ∃ x3 . and (In x3 x0) (x1 x3 = x2).
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with
x0,
0,
x1,
x0 = 0 leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H4:
∀ x2 . In x2 x0 ⟶ In (x1 x2) 0.
Assume H5:
∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3.
Apply unknownprop_fe7ff313be3d0b9f2334c12982636aff94f7603137e8053506a95c79965309c2 with
x0.
Let x2 of type ι be given.
Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with
x2,
x0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x1 x2.
Apply H4 with
x2.
The subproof is completed by applying H6.