proposition: Lemma subst_env_cont_subst_comp M G x (MG: correct_subst M G) T : G |-> x/T -> env (subst MG) = env (subst MG) [+] env T.
proof: Proof. intro GT. rewrite subst_env. destruct MG. set (q := subst_comp_env GT envs_c0). rewrite env_sum_assoc. congruence. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)