proposition: Lemma conv_term_ext : forall M N Q Q', conv_term M N Q -> Q' |=> Q -> conv_term M N Q'.
proof: Proof. induction M; intros; destruct N; inversion H. constructor; apply H0; trivial. constructor. constructor. eapply IHM; eauto. apply envSubst_lift1_ext; trivial. constructor. eapply IHM1; eauto. eapply IHM2; eauto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)