Let x0 of type ι → ο be given.
Assume H0:
not (∀ x1 . x0 x1).
Apply dneg with
∃ x1 . not (x0 x1).
Assume H1:
not (∃ x1 . not (x0 x1)).
Apply H0.
Let x1 of type ι be given.
Apply dneg with
x0 x1.
Apply not_ex_all_demorgan_i with
λ x2 . not (x0 x2),
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.