proposition: Lemma pair_falsehood (C : ComplementaryPair) : Part2 C -> isFalse C.
proof: Proof. intros q. unpack_pair C P Q con c; unfold isFalse, hfiber, Part1, Part2, chooser in *; simpl in *. induction c as [p|q']. - apply fromempty. contradicts (con p) q. - now exists q'. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Tactics