proposition: Theorem refl_trans_1n_trace_trans : forall step (a b c : A) (os os' : list trace), refl_trans_1n_trace step a b os -> refl_trans_1n_trace step b c os' -> refl_trans_1n_trace step a c (os ++ os').
proof: Proof. Proof using. intros. induction H; simpl; auto. concludes. rewrite <- app_assoc. constructor 2 with x'; auto. Qed.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)