Let z be given.

Assume Hz.

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 Lcp0z: F (conj (proj0 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We will prove proj1 (pa (conj (proj0 z)) (- proj1 z)) = - proj1 z.

An exact proof term for the current goal is CD_proj1_2 (conj (proj0 z)) (- proj1 z) ?? ??.

∎