Apply In_ind with
λ x0 . Inj1 x0 ⊆ V_ (ordsucc (9d271.. x0)).
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply Inj1E with
x0,
x1,
x1 ∈ V_ ((λ x2 . ordsucc (9d271.. x2)) x0) leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H2: x1 = 0.
Apply H2 with
λ x2 x3 . x3 ∈ V_ ((λ x4 . ordsucc (9d271.. x4)) x0).
Apply unknownprop_283f8fc5ea1a3c99f01ef684040d36f3b3e77f532f79e28eeabcc4dccf9b7028 with
9d271.. x0,
0.
The subproof is completed by applying Subq_Empty with
V_ (9d271.. x0).
Assume H2:
∃ x2 . and (x2 ∈ x0) (x1 = Inj1 x2).
Apply H2 with
x1 ∈ V_ ((λ x2 . ordsucc (9d271.. x2)) x0).
Let x2 of type ι be given.
Assume H3:
(λ x3 . and (x3 ∈ x0) (x1 = Inj1 x3)) x2.
Apply H3 with
x1 ∈ V_ ((λ x3 . ordsucc (9d271.. x3)) x0).
Assume H4: x2 ∈ x0.
Apply H5 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 H4.
Apply H0 with
x2.
The subproof is completed by applying H4.