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