Let x0 of type ι be given.
Let x1 of type ι be given.
Apply ReplE_impred with
x0,
λ x2 . (λ x3 . SetAdjoin x3 (Sing 1)) x2,
(λ x2 . SetAdjoin x2 (Sing 1)) x1,
x1 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Assume H3: x2 ∈ x0.
Claim L5: x1 = x2
Apply tagged_eqE_eq with
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H1.
Apply ordinal_Hered with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply L5 with
λ x3 x4 . x4 ∈ x0.
The subproof is completed by applying H3.