Let A and B be given.
Assume H: ¬ (A → B).
Apply andI to the current goal.
Apply dneg to the current goal.
Assume HnA: ¬ A.
Apply H to the current goal.
Assume a: A.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnA a).
Assume HB: B.
Apply H to the current goal.
Assume _: A.
An exact proof term for the current goal is HB.
∎