Let x0 of type ι be given.
Let x1 of type ι be given.
Apply Inj0E with
x0,
x1,
x1 ∈ V_ ((λ x2 . ordsucc (9d271.. x2)) x0) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H1:
(λ x3 . and (x3 ∈ x0) (x1 = Inj1 x3)) x2.
Apply H1 with
x1 ∈ V_ ((λ x3 . ordsucc (9d271.. x3)) x0).
Assume H2: x2 ∈ x0.
Apply H3 with
λ x3 x4 . x4 ∈ V_ ((λ x5 . ordsucc (9d271.. x5)) x0).
Apply V_I with
Inj1 x2,
(λ x3 . ordsucc (9d271.. x3)) x2,
(λ x3 . ordsucc (9d271.. x3)) x0 leaving 2 subgoals.
Apply ordinal_ordsucc_In with
9d271.. x0,
9d271.. x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_1ec7349a6007c1951cbc9535ca5769b83316f6778bed19ab211854c4c6028c5d with x0.
Apply unknownprop_24ba76162cbabacbe8136cf5d6f6295437383ecf4b3946427a5b4b7d60ed1941 with
x2,
x0.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_7520792d9c4001bd88f3e8a251d89ba23341c4c0a08e5856d9d9558b1998ce5c with x2.