proposition: Lemma trace_prefix_app A (t t' : trace A) : trace_prefix t (trace_app t t').
proof: Proof. destruct t, t'; ins; unfold trace_prepend; desf; eauto using nth_indep; done. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription