proposition: Lemma subst_ran_component_comp : forall G x T, G |-> x/T -> subst_envs_comp G -> forall p A, env T |= p := A -> subst_ran G |= p := A.
proof: Proof. induction G. destruct x; try_solve. destruct a. rewrite subst_ran_cons_some. destruct x; intros T Gx envsc p A Tp. inversion Gx. destruct (isVarDecl_dec (subst_ran G) p) as [[B Gp] | Gpn]. apply env_sum_ry. rewrite <- H0 in Tp. rewrite (subst_envs_comp_head envsc Tp Gp); trivial. apply env_sum_ly_rn; trivial. apply env_sum_ry. apply IHG with x T; try_solve. apply subst_envs_comp_tail with (Some t); trivial. rewrite subst_ran_cons_none. destruct x; try_solve. intros T Gx envc_G. apply (IHG x T); trivial. eapply subst_envs_comp_tail; eauto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)