proposition: Lemma terms_conv_extend_subst : forall M N Q Q', M ~(Q) N -> Q' |=> Q -> M ~(Q') N.
proof: Proof. intros. destruct H. constructor. apply conv_term_ext with Q; trivial. apply conv_env_ext with Q; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)