proposition: Lemma steps_renE xi M N : clos_refl_trans term step (ren xi M) N -> exists N', N = ren xi N' /\ clos_refl_trans term step M N'.
proof: Proof. move E: (ren xi M) => M' /clos_rt_rt1n_iff H. elim: H xi M E. { move=> > <-. eexists. split;[done|]. by apply: rt_refl. } move=> > +++ > ?. subst. move=> /step_renE [?] [->] ? _. move=> /(_ _ _ eq_refl) [?] [->] ?. eexists. split; [done|]. apply: rt_trans; [apply: rt_step|]; eassumption. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect