Let x0 of type ι → ι be given.
Apply unknownprop_fe7ff313be3d0b9f2334c12982636aff94f7603137e8053506a95c79965309c2 with
Repl 0 (λ x1 . x0 x1).
Let x1 of type ι be given.
Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with
x1,
Repl 0 (λ x2 . x0 x2).
Assume H0:
In x1 (Repl 0 (λ x2 . x0 x2)).
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with
0,
x0,
x1,
False leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H2: x1 = x0 x2.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x2.
The subproof is completed by applying H1.