Apply (func_ext set set) to the current goal.

Let x be given.

Use symmetry.

We will prove 1 + x = Inj1 x.

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

∎