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