Definition dnegelim {P Q : UU} : complementary P Q -> ¬¬ P -> P. Proof. intros c nnp. induction c as [n c]. induction c as [p|q]. - assumption. - contradicts nnp (λ p, n p q). Defined.
Require Import UniMath.MoreFoundations.Tactics.