proposition: Lemma steps_anti_ren delta s t: ren delta s >* t -> exists t', s >* t' /\ t = ren delta t'.
proof: Proof. remember (ren delta s) as s'. intros H; revert s Heqs'; induction H. - intros; subst. exists s; eauto. - intros; subst. eapply step_anti_ren in H as []; intuition. edestruct (IHstar x); intuition. exists x0; eauto. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun