proposition: Lemma trace_appA A (t t' t'' : trace A) : trace_app (trace_app t t') t'' = trace_app t (trace_app t' t'').
proof: Proof. unfold trace_app; ins; desf; try by rewrite appA. all: f_equal; extensionality x; desf. by rewrite trace_prepend_app. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription