Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι be given.
Assume H1:
∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ x1 x3 = x2 x3.
Claim L2:
{x1 x3|x3 ∈ SNoR x0} = {x2 x3|x3 ∈ SNoR x0}Apply ReplEq_ext with
SNoR x0,
λ x3 . x1 x3,
λ x3 . x2 x3.
Let x3 of type ι be given.
Apply H1 with
x3.
Apply SNoR_SNoS with
x0,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Claim L3:
{x1 x3|x3 ∈ SNoL x0} = {x2 x3|x3 ∈ SNoL x0}Apply ReplEq_ext with
SNoL x0,
λ x3 . x1 x3,
λ x3 . x2 x3.
Let x3 of type ι be given.
Apply H1 with
x3.
Apply SNoL_SNoS with
x0,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply L2 with
λ x3 x4 . SNoCut x4 {x1 x5|x5 ∈ SNoL x0} = SNoCut {x2 x5|x5 ∈ SNoR x0} {x2 x5|x5 ∈ SNoL x0}.
Apply L3 with
λ x3 x4 . SNoCut {x2 x5|x5 ∈ SNoR x0} x4 = SNoCut {x2 x5|x5 ∈ SNoR x0} {x2 x5|x5 ∈ SNoL x0}.
Let x3 of type ι → ι → ο be given.
The subproof is completed by applying H4.
Apply SNo_rec_i_eq with
λ x0 . λ x1 : ι → ι . SNoCut {x1 x2|x2 ∈ SNoR x0} {x1 x2|x2 ∈ SNoL x0}.
The subproof is completed by applying L0.