proposition: Lemma subst_cons_empty G : isEmptySubst G -> isEmptySubst (None::G).
proof: Proof. intros Ge x; destruct x; unfold varIsNotSubst. auto. apply (Ge x). Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)