proposition: Lemma subst_ran_empty : forall G, isEmptySubst G -> subst_ran G = EmptyEnv.
proof: Proof. induction G; auto. destruct a. intro f; destruct (f 0); discr. intro Ge. rewrite subst_ran_cons_none. apply IHG. apply subst_tail_empty; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)