proposition: Lemma lower_subst : forall M N G (M0: env M |= 0 :!) (MG: correct_subst N G) (MG': correct_subst M (None :: lift_subst G 1)) (MG'0: env (subst MG') |= 0 :! := (subst_at0 G MG' M0)), N = lower M M0 -> subst MG = lower (subst MG') MG'0.
proof: Proof. intros. apply term_eq; autorewrite with terms; rewrite H; autorewrite with terms. destruct M as [envM ???]. autorewrite with terms using simpl. unfold loweredEnv; simpl. destruct (subst_empty_dec G). destruct envM; simpl. autorewrite with terms; trivial. autorewrite with terms datatypes; trivial. destruct o; autorewrite with datatypes; trivial. destruct envM; simpl. autorewrite with datatypes terms. destruct (subst_ran G); trivial. destruct o; autorewrite with datatypes terms using simpl; trivial. unfold presubst, prelower. apply (lower_subst_aux M G M0). Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)