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 Lcp0w: F (conj (proj0 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1w: F (conj (proj1 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0zp0w: F (proj0 z * proj0 w).

Apply F_mul 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 Lcp1wp1z: F (conj (proj1 w) * proj1 z).

Apply F_mul 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 Lcp1wp1z: F (- conj (proj1 w) * proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzwL: F (proj0 z * proj0 w + - conj (proj1 w) * proj1 z).

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 Lp1wp0z: F (proj1 w * proj0 z).

Apply F_mul 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 Lp1zcp0w: F (proj1 z * conj (proj0 w)).

Apply F_mul 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 LzwR: F (proj1 w * proj0 z + proj1 z * conj (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 ??.

An exact proof term for the current goal is CD_proj0_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ??.

∎