Let z and w be given.
Assume Hz Hw.
Assume H1 H2.
Use transitivity with and (pa (proj0 z) (proj1 z)).
An exact proof term for the current goal is CD_proj0proj1_eta z Hz.
Use transitivity with and (pa (proj0 w) (proj1 w)).
rewrite the current goal using H1 (from left to right).
rewrite the current goal using H2 (from left to right).
Use reflexivity.
Use symmetry.
An exact proof term for the current goal is CD_proj0proj1_eta w Hw.
∎