proposition: Lemma subst_disjoint_c M G P (S: correct_subst M (lift_subst (None::G) 1)) (S': correct_subst (subst S) {x/P}) : correct_subst M (Some P::lift_subst G 1).
proof: Proof. inversion S; inversion S'. simpl in * . rewrite subst_env in dom_c1. rewrite subst_env in ran_c1. rewrite subst_ran_cons_none in dom_c1. rewrite subst_ran_cons_none in ran_c0. rewrite subst_ran_cons_none in ran_c1. split. assert (P_comp_MR: forall Ti Tj q, (Some P :: lift_subst G 1) |-> 0 / Ti -> (Some P :: lift_subst G 1) |-> (Datatypes.S q) / Tj -> env Ti [<->] env Tj). intros Ti Tj q Gp Gq p A B PA MB; destruct p. destruct (nth_lift_normal G 1 q Gq) as [T_j Tj_lift Tj_nth]. rewrite Tj_lift in MB. rewrite lift_env in MB; try_solve. inversion Gp. rewrite <- H0 in PA. apply (ran_c1 (Datatypes.S p)). rewrite subst_ran_single. destruct (env P); try_solve. replace (e [-] nil) with e. destruct o; try_solve. destruct e; try destruct o0; try_solve. apply env_sum_ry. assert (Gq_Tj: lift_subst G 1 |-> q / Tj). try_solve. rewrite (subst_comp_env Gq_Tj). apply env_sum_ry; trivial. eapply subst_envs_comp_tail; eauto. intros p q Ti Tj Gp Gq. destruct p. destruct q; try_solve. inversion Gp; inversion Gq. apply P_comp_MR with q; trivial. destruct q. apply env_comp_sym. apply P_comp_MR with p; trivial. apply (envs_c0 (Datatypes.S p) (Datatypes.S q)); try_solve. simpl; intros p A B. destruct p. intros A_typeP MB. apply (dom_c1 0); try_solve. apply env_sum_ly_rn; trivial. apply env_sub_ly_rn; auto with terms. apply subst_ran_lifted_noDecl. intros Gp Mp. apply (dom_c0 (Datatypes.S p)); try_solve. simpl in * . intros p A B RA MB. destruct p. destruct (subst_ran (Some P :: lift_subst G 1)); try_solve. destruct o; try_solve. destruct (env_sub_varDecl _ _ RA) as [PGr_p Gd_p]. rewrite subst_ran_cons_some in PGr_p. destruct (env_sum_varDecl _ _ PGr_p) as [[P_p Gr_p] | Gr_p]. apply (ran_c1 (Datatypes.S p)). apply env_sub_ly_rn; try_solve. rewrite subst_ran_single; trivial. destruct p; try_solve. apply env_sum_ly_rn; trivial. apply env_sub_ly_rn; trivial. apply (ran_c0 (Datatypes.S p)); trivial. apply env_sub_ly_rn; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)