proposition: Lemma trace_prefixE A (t t' : trace A) : trace_prefix t t' <-> exists t'', t' = trace_app t t''.
proof: Proof. split; ins; desf; eauto using trace_prefix_app. destruct t, t'; ins; desf; desf. - by eexists (trace_fin _). - exists (trace_inf (fun x => fl (x + length l))). unfold trace_prepend; f_equal; extensionality y; desf; eauto. f_equal; lia. - exists (trace_fin nil); f_equal; extensionality x; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription