proposition: Lemma trace_app_assoc A (t t' t'' : trace A) : trace_app t (trace_app t' t'') = trace_app (trace_app t t') t''.
proof: Proof. symmetry; apply trace_appA. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription