[STATEMENT]
lemma eta_reds_appL: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t \<Longrightarrow> s $ u \<rightarrow>\<^sub>\<eta>\<^sup>* t $ u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<rightarrow>\<^sub>\<eta>\<^sup>* t \<Longrightarrow> s $ u \<rightarrow>\<^sub>\<eta>\<^sup>* t $ u
[PROOF STEP]
by (induction s t rule: rtranclp.induct) (auto simp add: rtranclp.rtrancl_into_rtrancl)