We will prove HSNo (pa 0 i).

Apply HSNo_I to the current goal.

An exact proof term for the current goal is CSNo_0.

An exact proof term for the current goal is CSNo_Complex_i.

∎