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