Let x0 of type ι be given.

Let x1 of type ι be given.

Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with Inj0 x0 = Inj1 x1.

Assume H0: Inj0 x0 = Inj1 x1.

Claim L1: In 0 (Inj1 x1)

The subproof is completed by applying unknownprop_9998e40d8c081bcb0998eee5b18bc644807c64b4a7795024462a6db641b5bcc2 with x1.

Claim L2: In 0 (Inj0 x0)

Apply H0 with λ x2 x3 . In 0 x3.

The subproof is completed by applying L1.

Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with 0.

Apply unknownprop_993af6114ae86d533b92ae8c379a80f32d0d6d215834c9194ed09e506217bf3f with x0, 0, λ x2 . In 0 x2 leaving 2 subgoals.

The subproof is completed by applying L2.

Let x2 of type ι be given.

Assume H3: In x2 x0.

The subproof is completed by applying unknownprop_9998e40d8c081bcb0998eee5b18bc644807c64b4a7795024462a6db641b5bcc2 with x2.

■

Proofgold Proof