proposition: Lemma complementaryDecisions (C : ComplementaryPair) : iscontr (isTrue C ⨿ isFalse C).
proof: Proof. intros. apply iscontrifweqtounit. assert (w := weqcoprodsplit (λ _:unit, chooser C)). apply invweq. apply (weqcomp w). apply weqcoprodf; apply weqhfiberunit. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Tactics