proposition: Lemma prod_m_ext : Proper (XSet.Equal ==> XSet.Equal ==> eq ==> eq ==> iff) prod.
proof: Proof. intros s s' ss' t t' tt' a a' aa' b b' bb'. unfold prod. rewrite ss', tt', aa', bb'. refl. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)