proposition: Lemma subst_comp_comp_ran G x T : G |-> x/T -> subst_envs_comp G -> env T [<->] subst_ran G.
proof: Proof. intros GxT Gc p A B Tp Gp. set (w := subst_ran_component_comp GxT Gc Tp). unfold VarD in *; congruence. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)