proposition: Lemma subst_env_compat M G x T (MG: correct_subst M G) : G |-> x / T -> env (subst MG) [<->] env T.
proof: Proof. intro GxT. inversion MG. assert (TG: env T [<->] subst_ran G). apply subst_comp_comp_ran with x; trivial. rewrite subst_env. intros p A B LA RB. set (w := subst_ran_component_comp GxT envs_c0 RB). set (w' := env_sum_ry (env M [-] subst_dom G) w). unfold VarD in *; congruence. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)