proposition: Lemma subst_empty_dec : forall G, {isEmptySubst G} + {~isEmptySubst G}.
proof: Proof. induction G. left; apply subst_nil_empty. destruct a. right; unfold isEmptySubst; intro f. absurd ((Some t::G) |-> 0/-); auto. compute; intro f'; destruct f'; discr. destruct IHG. left; apply subst_cons_empty; trivial. right. intro f. absurd (isEmptySubst G); trivial. unfold isEmptySubst; intro x; apply (f (S x)). Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)