proposition: Lemma isaprop_isFalse (C : ComplementaryPair) : isaprop (isFalse C).
proof: Proof. intros. apply (isapropcomponent2 (isTrue C) (isFalse C)). apply isapropifcontr. apply complementaryDecisions. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Tactics