proposition: Lemma subst_comp_env : forall G x T, G |-> x/T -> subst_envs_comp G -> subst_ran G = subst_ran G [+] env T.
proof: Proof. induction G. destruct x; try_solve. intros x T aG_xT envsc_aG. destruct a. rewrite subst_ran_cons_some. destruct x. assert (Tt: t = T). unfold varSubstTo in *; simpl in *. inversion aG_xT; trivial. rewrite Tt. rewrite env_comp_sum_comm. rewrite env_sum_assoc. rewrite env_sum_double; trivial. apply env_comp_sum_comp_right with (env t). rewrite <- subst_ran_cons_some. apply subst_comp_comp_ran with 0; trivial. rewrite env_sum_assoc. assert (G_GT: subst_ran G = subst_ran G [+] env T). apply (IHG x T); auto. apply subst_envs_comp_tail with (Some t); trivial. congruence. rewrite subst_ran_cons_none. destruct x. try_solve. apply (IHG x T); try_solve. eapply subst_envs_comp_tail; eauto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)