Apply unknownprop_7eb4c3a1a6214b539c51293d93cead859462369dd6722562a2c356882dd33f28 with λ x0 x1 : ι → ι . ∀ x2 . x1 x2 = Repl (setminus x2 (Sing 0)) (λ x3 . x1 x3).

Claim L0: ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3) ⟶ Repl (setminus x0 (Sing 0)) (λ x3 . x1 x3) = Repl (setminus x0 (Sing 0)) (λ x3 . x2 x3)

Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι → ι be given.

Assume H0: ∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3.

Apply unknownprop_4e431d17235033fd023e568086fb9fd6f3a2be9883f5e2300fe470ca304ea26a with setminus x0 (Sing 0), x1, x2.

Let x3 of type ι be given.

Assume H1: In x3 (setminus x0 (Sing 0)).

Apply H0 with x3.

Apply unknownprop_29bb348fa91dd336b68009f32eb9809a20ab7c7920c130047ad13aae3b335ac5 with x0, Sing 0, x3.

The subproof is completed by applying H1.

Apply unknownprop_b46ce29ff1d7f9d2e6d60e6a0f6f0736a07c8ba94a4f18feca3e51921a7ff153 with λ x0 . λ x1 : ι → ι . Repl (setminus x0 (Sing 0)) (λ x2 . x1 x2).

The subproof is completed by applying L0.

■

Proofgold Proof