proposition: Lemma correct_subst_lift : forall M N G (M0: env M |= 0 :!), correct_subst N G -> N = lower M M0 -> correct_subst M (None :: lift_subst G 1).
proof: Proof. intros ???? [envNG domNG ranNG] H. rewrite H in domNG. rewrite H in ranNG. rewrite lower_env in domNG. rewrite lower_env in ranNG. clear H. constructor. apply subst_envs_comp_cons. apply lifted_subst_envs_comp; trivial. destruct (env M). apply env_comp_empty. destruct o. destruct M0; try_solve. simpl. rewrite subst_dom_lifted. apply env_comp_cons; auto. unfold loweredEnv in domNG. simpl in domNG. rewrite finalSeg_cons in domNG; trivial. simpl. rewrite subst_ran_cons_none. rewrite subst_dom_lifted. destruct (subst_empty_dec G). rewrite subst_ran_lifted_empty; trivial. simpl; apply env_comp_sym; apply env_comp_empty. rewrite subst_ran_lifted_ne; trivial. simpl. destruct (env M). apply env_comp_empty. destruct o. destruct M0; try_solve. apply env_comp_cons; auto. unfold loweredEnv in ranNG. simpl in ranNG. rewrite finalSeg_cons in ranNG; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)