proposition: Lemma step_renE xi M N : step (ren xi M) N -> exists N', N = ren xi N' /\ step M N'.
proof: Proof. move E: (ren xi M) => M' H. elim: H xi M E. - move=> ??? [] //. move=> [] // ?? /= [<- <-]. eexists. split; first last. { by apply: stepSubst. } rewrite !simpl_term. apply: ext_subst_term. by case. - move=> > ? IH ? [] //= ?? [??]. subst. have [? [? ?]] := IH _ _ eq_refl. subst. eexists. split; first last. { apply: stepAppL. eassumption. } done. - move=> > ? IH ? [] //= ?? [??]. subst. have [? [? ?]] := IH _ _ eq_refl. subst. eexists. split; first last. { apply: stepAppR. eassumption. } done. - move=> > ? IH ? [] //= ? [?]. subst. have [? [? ?]] := IH _ _ eq_refl. subst. eexists. split; first last. { apply: stepLam. eassumption. } done. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect