Let P be given.

Assume u: ¬ ∀x, P x.

Apply dneg to the current goal.

Assume v: ¬ ∃x, ¬ P x.

Apply u to the current goal.

Let x be given.

Apply dneg to the current goal.

Assume w: ¬ P x.

An exact proof term for the current goal is (not_ex_all_demorgan_i (λx ⇒ ¬ P x) v x w).

∎