proposition: Lemma steps'AppL {s s' t} : steps' s s' -> steps' (app s t) (app s' t).
proof: Proof. elim. - move=> *. apply: rt_step. by apply: step'AppL. - move=> *. by apply: rt_refl. - move=> *. by apply: rt_trans; eassumption. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun