proposition: Lemma subst_envs_comp_tail a G : subst_envs_comp (a::G) -> subst_envs_comp G.
proof: Proof. intros envc_aG p q Ti Tj p_neq_q Gp Gq. apply (envc_aG (S p) (S q)); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)