proposition: Lemma conv_by : forall M N Q, M ~(Q) N -> M ~ N.
proof: Proof. intros. exists Q; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)