proposition: Lemma subst_at0 : forall M G (MG: correct_subst M (None :: lift_subst G 1)), env M |= 0 :! -> env (subst MG) |= 0 :! .
proof: Proof. intros. rewrite subst_env. destruct (env M). rewrite subst_ran_cons_none. destruct (subst_empty_dec G); simpl. rewrite subst_ran_lifted_empty; trivial. rewrite subst_ran_lifted_ne; solve [trivial | constructor 2; trivial]. destruct o. destruct H; try_solve. simpl. rewrite subst_ran_cons_none. destruct (subst_empty_dec G); simpl. rewrite subst_ran_lifted_empty; trivial. rewrite subst_ran_lifted_ne; solve [trivial | constructor 2; trivial]. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)