Apply (func_ext set set) to the current goal.

Let x be given.

Use symmetry.

We will prove 0 + x = Inj0 x.

An exact proof term for the current goal is (Inj0_setsum_0L x).

∎