Let z and w be given.
Assume Hz Hw.
We prove the intermediate claim Lp0z: F (proj0 z).
An
exact proof term for the current goal is
CD_proj0R z Hz.
We prove the intermediate claim Lp1z: F (proj1 z).
An
exact proof term for the current goal is
CD_proj1R z Hz.
We prove the intermediate claim Lp0w: F (proj0 w).
An
exact proof term for the current goal is
CD_proj0R w Hw.
We prove the intermediate claim Lp1w: F (proj1 w).
An
exact proof term for the current goal is
CD_proj1R w Hw.
We will
prove pa (proj0 z + proj0 w) (proj1 z + proj1 w) = pa (proj0 w + proj0 z) (proj1 w + proj1 z).
Use f_equal.
Apply F_add_com to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply F_add_com to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.