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