proposition: Lemma eval_steps' s t : L.eval s t -> steps' s t.
proof: Proof. elim. { move=> ?. by apply: rt_refl. } move=> {}s s' {}t t' u' _ Hss' /eval_is_lam [t''] -> Htt' _ H. apply: rt_trans; [|eassumption]. apply: rt_trans. { by apply: (steps'AppL Hss'). } apply: rt_trans. { by apply: (steps'AppR Htt'). } apply: rt_step. by apply: step'App. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun