Let z be given.

Assume Hz.

Apply CD_proj1_1 z Hz to the current goal.

An exact proof term for the current goal is (λH _ ⇒ H).

∎