proposition: Lemma envSubst_eq_abs : forall M N (Mabs: isAbs M) (Nabs: isAbs N) (MN: env M [<->] env N) (MNin: env (absBody Mabs) [<->] env (absBody Nabs)), envSubst_lift1 (compEnvSubst MN) <=> compEnvSubst MNin.
proof: Proof. intros M N Mabs Nabs MN MNin; constructor; intros i j; term_inv M; term_inv N. set (hint := MNin 0 A A0). destruct i; destruct j; firstorder auto with zarith. set (hint := MNin 0 A A0). destruct i; destruct j; try contr. split_all. ex A. fo. ex A0. fo. split_all. subst j. ex x0. fo. ex x. fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)