proposition: Lemma RTn1_step : forall (step : step_relation) x y z l l', step x y l -> refl_trans_n1_trace step y z l' -> refl_trans_n1_trace step x z (l ++ l').
proof: Proof. Proof using. intros. induction H0. - rewrite app_nil_r. rewrite <- app_nil_l. econstructor. constructor. auto. - concludes. rewrite app_assoc. econstructor; eauto. Qed.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)