proposition: Lemma lift_inj (A B : term) : A.[ren(+1)] = B.[ren(+1)] -> A = B.
proof: Proof. intros H. apply (f_equal (subst (ren pred))) in H. asimpl in H. unfold funcomp, lift in H. now asimpl in H. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics