Lemma isaprop_isFalse (C : ComplementaryPair) : isaprop (isFalse C). Proof. intros. apply (isapropcomponent2 (isTrue C) (isFalse C)). apply isapropifcontr. apply complementaryDecisions. Defined.
Require Import UniMath.MoreFoundations.Tactics.