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