Definition decidableAnd (P Q : DecidableProposition) : DecidableProposition. Proof. intros. exists (P × Q). apply isdecpropdirprod; apply decidabilityProperty. Defined.
Require Import UniMath.MoreFoundations.Tactics.