proposition: Lemma redLe_app_helperR s t t' u i j: t >(<= i) t' -> app s t' >(<=j) u -> app s t >(<=i+j) u.
proof: Proof. intros ? H'. eapply redLe_app_helper in H'. 3:eassumption. 2:Lreflexivity. eassumption. Qed.
imports: Undecidability.L(Tactics.Computable Lproc Lbeta)