proposition: Lemma lift_injn (A B : term) n : A.[ren(+n)] = B.[ren(+n)] -> A = B.
proof: Proof. induction n. autosubst. rewrite (@renS A), (@renS B). intros H. apply lift_inj in H. auto. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics