Claim L0:
∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ binunion (Sing 0) {x1 x3|x3 ∈ x0} = binunion (Sing 0) {x2 x3|x3 ∈ x0}Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι be given.
Assume H0: ∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3.
Claim L1: {x1 x3|x3 ∈ x0} = {x2 x3|x3 ∈ x0}
Apply ReplEq_ext with
x0,
x1,
x2.
The subproof is completed by applying H0.
Apply L1 with
λ x3 x4 . binunion (Sing 0) x4 = binunion (Sing 0) {x2 x5|x5 ∈ x0}.
Let x3 of type ι → ι → ο be given.
The subproof is completed by applying H2.
Apply In_rec_i_eq with
λ x0 . λ x1 : ι → ι . binunion (Sing 0) {x1 x2|x2 ∈ x0}.
The subproof is completed by applying L0.