proposition: Lemma anti_ren delta s t: Injective delta -> ren delta s = ren delta t -> s = t.
proof: Proof. intros H; induction s in delta, H, t |-*; destruct t; try discriminate. all: cbn; injection 1; intros; subst; eauto. - erewrite IHs. 3: eapply H1. eauto. eapply injective_upRen_exp_exp; eauto. - erewrite IHs1, IHs2; eauto. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun