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 prove the intermediate
claim Lp0zw:
F (proj0 z + proj0 w).
Apply F_add to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim Lp1zw:
F (proj1 z + proj1 w).
Apply F_add to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An
exact proof term for the current goal is
CD_proj0_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ??.