We prove the intermediate claim L1: ∀x y z, SNo x → SNo y → SNo z → (x + y) + z = x + (y + z).

Let x, y and z be given.

Assume Hx Hy Hz.

Use symmetry.

An exact proof term for the current goal is add_SNo_assoc x y z Hx Hy Hz.

Apply CD_add_assoc {2} SNo complex_tag_fresh add_SNo SNo_add_SNo L1 to the current goal.

∎