Lemma pair_falsehood (C : ComplementaryPair) : Part2 C -> isFalse C. 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.
Require Import UniMath.MoreFoundations.Tactics.