proposition: Lemma double_subst : forall M G P (MP: correct_subst M {x/P}) (MPG: correct_subst (subst MP) (None :: lift_subst G 1)) (MG: correct_subst M (None :: lift_subst G 1)) (PG: correct_subst P (None :: lift_subst G 1)) (MGP: correct_subst (subst MG) {x/subst PG}), subst MPG = subst MGP.
proof: Proof. intros. apply term_eq. autorewrite with terms. cut (tail (env M) [+] tail (env P) [-] subst_dom G [+] subst_ran G = tail (env M) [-] subst_dom G [+] subst_ran G [+] (tail (env P) [-] subst_dom G [+] subst_ran G)). destruct (subst_empty_dec G). destruct (env M); destruct (env P); try destruct o; try destruct o0; simpl; (autorewrite with terms using simpl); try_solve. destruct (env M); destruct (env P); try destruct o; try destruct o0; simpl; (autorewrite with terms using simpl); try destruct (subst_ran G); try destruct (subst_dom G); try destruct e; try destruct o; try destruct o0; try_solve. rewrite env_sum_assoc. rewrite <- (env_sum_assoc (subst_ran G)). rewrite env_sum_remove_double. rewrite <- env_sum_assoc. rewrite env_sub_move; trivial. autorewrite with terms datatypes. unfold presubst. set (w := double_subst_aux (term M) G 0 PG). simpl in w; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)