proposition: Lemma step_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 in delta |-*. all: intros []; try discriminate; injection 1; intros; subst. - destruct e; try discriminate; injection H1; intros; subst. exists (beta e e0); intuition. now asimpl. - edestruct IHstep; eauto. intuition; subst. exists (lambda x). intuition. - edestruct IHstep; eauto. exists (x e0); intuition; now subst. - edestruct IHstep; eauto. exists (e x); intuition; now subst. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun