proposition: Lemma subst_ran_lifted_empty : forall G, isEmptySubst G -> subst_ran (lift_subst G 1) = EmptyEnv.
proof: Proof. induction G; auto. intro aG_empty. destruct a. absurd ((Some t::G) |-> 0/-); auto. compute; intro f; destruct f; discr. unfold subst_ran; simpl. apply IHG. apply subst_tail_empty; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)