proposition: Lemma subst_ran_lifted_noDecl G : subst_ran (lift_subst G 1) |= 0 :! .
proof: Proof. destruct (subst_empty_dec G). rewrite subst_ran_lifted_empty; auto with terms. rewrite subst_ran_lifted_ne; auto with terms. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)