Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Assume H0:
∀ x2 . In x2 x0 ⟶ x1 x2.
Let x2 of type ι be given.
Apply unknownprop_a5b0141dc7f70dc45c7d1f61b8342a4e97134fda6aab3192ae08a7f3d8c44b7c with
λ x3 x4 : ι → ι . In x2 (x4 x0) ⟶ x1 x2.
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with
x0,
Repl x0 (λ x3 . (λ x4 . SetAdjoin x4 (Sing 1)) x3),
x2,
x1 x2 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0 with x2.
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with
x0,
λ x3 . (λ x4 . SetAdjoin x4 (Sing 1)) x3,
x2,
x1 x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Apply H5 with
λ x4 x5 . x1 x5.
Apply H1 with
x3.
The subproof is completed by applying H4.