proposition: Lemma subst_lift_empty G i : isEmptySubst G -> isEmptySubst (lift_subst G i).
proof: Proof. intros Ge x. destruct (Ge x); unfold varIsNotSubst. left; apply nth_lift_subst_n; trivial. right; apply nth_lift_subst_sn; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)