Definition decidableOr (P Q : DecidableProposition) : DecidableProposition. Proof. intros. exists (P ∨ Q). apply isdecprophdisj; apply decidabilityProperty. Defined.
Require Import UniMath.MoreFoundations.Tactics.