Definition pairDisjunction (C C' : ComplementaryPair) : ComplementaryPair. Proof. intros. exact (pairNegation (pairConjunction (pairNegation C) (pairNegation C'))). Defined.
Require Import UniMath.MoreFoundations.Tactics.