Library CoLoR.Util.Pair.PairUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-06-17
general results on pairs

Set Implicit Arguments.


Section S.

  Variables (A B : Type)
            (eqdecA : forall x y : A, {x=y}+{~x=y})
            (eqdecB : forall x y : B, {x=y}+{~x=y}).

  Lemma eq_pair_dec : forall x y : A*B, {x=y}+{~x=y}.

End S.