Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_4db127623a54dea607d4178c4cffe8099fa715d4dd5c11459d1bd4ea367db087 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_3069c6fa8dbd033f1c94555c93d580ac5c2fd979807cb20dbdb8dc4cc9b1517f with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_7963a4bf2feda239add5cf25163811bc2206f6f21a0e4a70277699970e74fa1e with
x0,
x1,
False leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι → ι be given.
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with
x0,
x1,
x2,
False leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H6:
∀ x3 . In x3 x0 ⟶ In (x2 x3) x1.
Assume H7:
∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
ordsucc x1,
x0.
Apply unknownprop_7750078cf23be1c80f04c25ad7cbaaf73ac1b6c9f1f54ab639cc8621b4808d18 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Apply H6 with
x3.
Apply L8 with
x3.
The subproof is completed by applying H9.
Claim L10:
∀ x3 . In x3 (ordsucc x1) ⟶ ∀ x4 . In x4 (ordsucc x1) ⟶ x2 x3 = x2 x4 ⟶ x3 = x4Let x3 of type ι be given.
Let x4 of type ι be given.
Apply H7 with
x3,
x4 leaving 2 subgoals.
Apply L8 with
x3.
The subproof is completed by applying H10.
Apply L8 with
x4.
The subproof is completed by applying H11.
Apply notE with
∀ x3 . In x3 (ordsucc x1) ⟶ ∀ x4 . In x4 (ordsucc x1) ⟶ x2 x3 = x2 x4 ⟶ x3 = x4 leaving 2 subgoals.
Apply unknownprop_51b06166fbaa8c1974a215921ab5f4fa4631b749f74b82b1341de0a30786dca9 with
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L9.
The subproof is completed by applying L10.