Let x0 of type ι be given.
Let x1 of type ι be given.
Apply tagged_not_ordinal with
x1.
Apply ordinal_Hered with
x0,
(λ x2 . SetAdjoin x2 (Sing 1)) x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.