proposition: Lemma rho_correct s t : proc s -> lambda t -> rho s t >* s (rho s) t.
proof: Proof. intros. unfold rho,r. redStep at 1. apply star_trans_l. now Lsimpl. Qed.
imports: Undecidability.L.Tactics(Lproc Lbeta Lrewrite Reflection) ListTactics