proposition: Lemma subst_envs_comp_single : forall T, subst_envs_comp {x/T}.
proof: Proof. unfold subst_envs_comp; intros. destruct i; destruct j; try solve [ inversion H; destruct i; simpl in *; discr | inversion H0; destruct j; simpl in *; discr ]. inversion H; inversion H0; rewrite <- H2; rewrite <- H3; apply env_comp_refl. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)