proposition: Lemma subst_envs_comp_singleton : forall G T, isSingletonSubst T G -> subst_envs_comp G.
proof: Proof. intros; intros i j Ti Tj Gi Gj. inversion H. destruct i; destruct j; try solve [ inversion Gj; destruct (H1 j); destruct G; try_solve | inversion Gi; destruct (H1 i); destruct G; try_solve ]. assert (Ti = Tj). inversion Gi; inversion Gj; destruct G; try_solve. rewrite H2; apply env_comp_refl. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)