Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Apply unknownprop_d4b086cd91c37b32bf1c8961308be7f50bc527a9bea045cb93ec3985b2d19bb6 with λ x3 x4 : ι → ι → ι . In x2 (x4 x0 x1) ⟶ or (∃ x5 . and (In x5 x0) (x2 = Inj0 x5)) (∃ x5 . and (In x5 x1) (x2 = Inj1 x5)).

Assume H0: In x2 (binunion (Repl x0 (λ x3 . Inj0 x3)) (Repl x1 (λ x3 . Inj1 x3))).

Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with Repl x0 (λ x3 . Inj0 x3), Repl x1 (λ x3 . Inj1 x3), x2, or (∃ x3 . and (In x3 x0) (x2 = Inj0 x3)) (∃ x3 . and (In x3 x1) (x2 = Inj1 x3)) leaving 3 subgoals.

The subproof is completed by applying H0.

Assume H1: In x2 (Repl x0 (λ x3 . Inj0 x3)).

Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with ∃ x3 . and (In x3 x0) (x2 = Inj0 x3), ∃ x3 . and (In x3 x1) (x2 = Inj1 x3).

Apply unknownprop_74e6ddb76e51f556d0e4a910f649c4782bc9cb375d38baef38a8c05a47e8ef22 with x0, Inj0, x2.

The subproof is completed by applying H1.

Assume H1: In x2 (Repl x1 (λ x3 . Inj1 x3)).

Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with ∃ x3 . and (In x3 x0) (x2 = Inj0 x3), ∃ x3 . and (In x3 x1) (x2 = Inj1 x3).

Apply unknownprop_74e6ddb76e51f556d0e4a910f649c4782bc9cb375d38baef38a8c05a47e8ef22 with x1, Inj1, x2.

The subproof is completed by applying H1.

■

Proofgold Proof