proposition: Lemma terms_conv_diff_env : forall M N N' Q, M ~(Q) N -> term N' = term N -> activeEnv N' = activeEnv N -> M ~(Q) N'.
proof: Proof. intros; destruct H; constructor. rewrite H0; trivial. intros x y xy A. rewrite H1. apply H2; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)