Let z, w and u be given.
Assume Hz Hw Hu.
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 Lp0u: F (proj0 u).
An
exact proof term for the current goal is
CD_proj0R u Hu.
We prove the intermediate claim Lp1u: F (proj1 u).
An
exact proof term for the current goal is
CD_proj1R u Hu.
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 ??.
We prove the intermediate
claim Lp0wu:
F (proj0 w + proj0 u).
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 Lp1wu:
F (proj1 w + proj1 u).
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 ??.
Set zw to be the term
pa (proj0 z + proj0 w) (proj1 z + proj1 w).
Set wu to be the term
pa (proj0 w + proj0 u) (proj1 w + proj1 u).
We will
prove pa (proj0 zw + proj0 u) (proj1 zw + proj1 u) = pa (proj0 z + proj0 wu) (proj1 z + proj1 wu).
rewrite the current goal using
CD_proj0_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).
rewrite the current goal using
CD_proj1_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).
rewrite the current goal using
CD_proj0_2 (proj0 w + proj0 u) (proj1 w + proj1 u) ?? ?? (from left to right).
rewrite the current goal using
CD_proj1_2 (proj0 w + proj0 u) (proj1 w + proj1 u) ?? ?? (from left to right).
Use f_equal.
Apply F_add_assoc 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 ??.
Apply F_add_assoc 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 ??.