proposition: Lemma term_build_conv_ext : forall M Q, exists Q', Q' |=> Q /\ exists M', M ~(Q') M' /\ envMinimal M'.
proof: Proof. intros. destruct (@term_build_conv M Q EmptyEnv) as [Q' [Q'Q [M' [MM' [_ [Mmin _]]]]]]. intros; inversion H1; destruct y; try_solve. exists Q'; split; trivial. exists M'; split; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)