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

Claim L0: ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3) ⟶ binunion (Sing 0) (Repl x0 (λ x3 . x1 x3)) = binunion (Sing 0) (Repl x0 (λ 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.

Claim L1: Repl x0 (λ x3 . x1 x3) = Repl x0 (λ x3 . x2 x3)

Apply unknownprop_4e431d17235033fd023e568086fb9fd6f3a2be9883f5e2300fe470ca304ea26a with x0, x1, x2.

The subproof is completed by applying H0.

Apply L1 with λ x3 x4 . binunion (Sing 0) x4 = binunion (Sing 0) (Repl x0 (λ x5 . x2 x5)).

Let x3 of type ι → ι → ο be given.

Assume H2: x3 (binunion (Sing 0) (Repl x0 x2)) (binunion (Sing 0) (Repl x0 x2)).

The subproof is completed by applying H2.

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

The subproof is completed by applying L0.

■

Proofgold Proof