proposition: Lemma typing_in_subst_env M G (C: correct_subst M G) x T : G |-> x/T -> subst_ran G |- term T := type T.
proof: Proof. intros. destruct C. rewrite (subst_comp_env H envs_c0). apply typing_ext_env_l. exact (typing T). Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)