Apply func_ext prop (prop → prop) to the current goal.
Let x be given.
Apply func_ext prop prop to the current goal.
Let y be given.
Apply prop_ext_2 to the current goal.
Assume H1: x ∨ y.
Assume H2: ¬ x ∧ ¬ y.
Apply H2 to the current goal.
Assume H3 H4.
An exact proof term for the current goal is (H1 False H3 H4).
Assume H1: ¬ (¬ x ∧ ¬ y).
Apply (xm x) to the current goal.
Assume H2: x.
Apply orIL to the current goal.
An exact proof term for the current goal is H2.
Assume H2: ¬ x.
Apply (xm y) to the current goal.
Assume H3: y.
Apply orIR to the current goal.
An exact proof term for the current goal is H3.
Assume H3: ¬ y.
Apply H1 to the current goal.
An exact proof term for the current goal is (andI (¬ x) (¬ y) H2 H3).
∎