proposition: Lemma steps'AppR {s t t'} : steps' t t' -> steps' (app (lam s) t) (app (lam s) t').
proof: Proof. elim. - move=> *. apply: rt_step. by apply: step'AppR. - move=> *. by apply: rt_refl. - move=> *. by apply: rt_trans; eassumption. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun