proposition: Lemma subst_disjoint M G P (S: correct_subst M (None :: lift_subst G 1)) (S': correct_subst (subst S) {x/P}) (Sj: correct_subst M (Some P :: lift_subst G 1)) : subst S' = subst Sj.
proof: Proof. apply term_eq. rewrite !subst_env, subst_ran_cons_none, subst_ran_single. simpl. rewrite env_sum_sub, env_sub_sub_sum. simpl. rewrite env_sum_empty_r, env_sum_assoc, (@env_comp_sum_comm (subst_ran (lift_subst G 1)) (env P)), subst_ran_cons_some; trivial. apply env_comp_sym. apply env_comp_sum_comp_right with (env P). rewrite <- subst_ran_cons_some. apply subst_comp_comp_ran with 0. unfold varSubstTo; trivial. destruct Sj; trivial. intro p; destruct p. destruct (subst_empty_dec G) as [Ge | Gne]. rewrite subst_ran_lifted_empty; trivial. left; left; trivial. rewrite subst_ran_lifted_ne; trivial. left; right; trivial. right; left; destruct p; trivial. rewrite !subst_term. change (None :: lift_subst G 1) with (lift_subst (None::G) 1). apply presubst_disjoint. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)