proposition: Lemma eq_prod_dec :(forall x y, {eqA x y}+{~eqA x y}) -> (forall x y, {eqB x y}+{~eqB x y}) -> forall x y, {eq_prod x y}+{~eq_prod x y}.
proof: Proof. rewrite /eq_prod => hA hB [a b] [a' b']. case: (hA a a') => hA'. case: (hB b b') => hB'. by left; split. right. case => _ hn. by apply: hB'. right. case => hn _. by apply: hA'. Defined.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)