proposition: Lemma conv_env_lifted : forall M N Q, conv_env M N Q -> conv_env (lift M 1) (lift N 1) (envSubst_lift1 Q).
proof: Proof. intros. intros x y Qxy A. rewrite (activeEnv_lift M 1). rewrite (activeEnv_lift N 1). unfold liftedEnv; autorewrite with datatypes terms using simpl. destruct x; destruct y. split; intro; inversion H0. exfalso; apply envSubst_lift1_absurdR with y Q; trivial. exfalso; apply envSubst_lift1_absurdL with x Q; trivial. assert (Q_xy: envSub Q x y). destruct Q; trivial. set (w := H x y Q_xy A). tauto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)