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