Definition pairConjunction (C C' : ComplementaryPair) : ComplementaryPair. Proof. unpack_pair C P Q con c; unpack_pair C' P' Q' con' c'; simpl in *. unfold ComplementaryPair. exists (P × P'); exists (Q ⨿ Q'). split. - simpl. intros a b. induction a as [p p']. induction b as [b|b]. + induction c' as [_|q']. * contradicts (con p) b. * contradicts (con p) b. + contradicts (con' p') b. - simpl. induction c as [p|q]. + induction c' as [p'|q']. * apply ii1. exact (p,,p'). * apply ii2, ii2. exact q'. + induction c' as [p'|q']. * apply ii2, ii1. exact q. * apply ii2, ii2. exact q'. Defined.
Require Import UniMath.MoreFoundations.Tactics.