proposition: Lemma lStep s t u: lambda t -> (subst' s 0 t) >* u -> (lam s) t >* u.
proof: Proof. intros. rewrite <- H0. apply step_star_subrelation. rewrite <- subst'_eq. now apply step_Lproc. Qed.
imports: Undecidability.L(ComputableTactics Lproc Tactics.Computable Lrewrite)