Let x0 of type ι be given.
Let x1 of type ι be given.
set y2 to be ...
set y3 to be ...
Apply unknownprop_023b2e512ed9c52f995f2d07c1a06cfb4ae27f29745759c860f7e880eac7d40f with
SNoLev y2,
λ x4 . In x4 y2 ⟶ In x4 y3 leaving 2 subgoals.
Let x4 of type ι be given.
Apply unknownprop_d4c6f9663742385071dd283da85a9397dc2dfd0eede50c9fd289b7b23ca97cdd with
In x4 y2,
In x4 y3 leaving 2 subgoals.
Apply H3 with
x4.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Let x4 of type ι be given.
Apply unknownprop_22b63889168c3c27321f1d9d99a6c13d916b48d833ad1ef7079baee20e0a05c6 with
In ((λ x5 . SetAdjoin x5 (Sing 1)) x4) y3,
In x4 y3,
In ((λ x5 . SetAdjoin x5 (Sing 1)) x4) y3 leaving 3 subgoals.
Apply H7 with
x4.
The subproof is completed by applying L10.
Assume H12:
not (In x4 y3).
The subproof is completed by applying H11.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
y2,
y3.
Let x4 of type ι be given.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
y2,
SNoElts_ (SNoLev y2),
x4 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H9.
Apply L8 with
x4 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying H9.
Apply unknownprop_e5ee05cdff8551ce0d9dc58ec4d6754afa2e75276323e770f74710c8b0d2eef5 with
SNoLev y2,
y2,
y3 leaving 2 subgoals.
The subproof is completed by applying L6.
Apply unknownprop_1ca53845812367e72c2bc5ec7e7af7cc89df4a229d3426c9251c15fa30be903b with
y2.
The subproof is completed by applying H1.
Apply unknownprop_e5ee05cdff8551ce0d9dc58ec4d6754afa2e75276323e770f74710c8b0d2eef5 with
SNoLev x0,
x0,
y2 leaving 2 subgoals.
The subproof is completed by applying L4.
Apply unknownprop_1ca53845812367e72c2bc5ec7e7af7cc89df4a229d3426c9251c15fa30be903b with
x0.
The subproof is completed by applying H0.