proposition: Lemma eqPair_dec : forall x y : pair, {eqPair x y} + {~eqPair x y}.
proof: Proof. intros. destruct (eqA_dec (fst x) (fst y)). destruct (eqB_dec (snd x) (snd y)). left. split; trivial. right. intro. destruct H. contr. right. intro. destruct H. contr. Defined.
imports: CoLoR(LogicUtil RelUtil RelExtras) Coq(Setoid Morphisms Basics)