Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0:
∀ x2 . In x2 x0 ⟶ In x2 x1.
Assume H1:
∀ x2 . In x2 x1 ⟶ In x2 x0.
Apply unknownprop_a23ec6a55ac212526d74cbf0d04096929ad453b0eb0f8023e32b8a33930d39fb with
x0,
x1 leaving 2 subgoals.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
x0,
x1.
The subproof is completed by applying H0.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
x1,
x0.
The subproof is completed by applying H1.