proposition: Lemma trace_in_app A (a : A) (t t' : trace A) : trace_elems (trace_app t t') a <-> trace_elems t a \/ trace_length t <> NOinfinity /\ trace_elems t' a.
proof: Proof. split; destruct t, t'; ins; unfold trace_prepend in *; desf; rewrite ?in_app_iff in *; desf; eauto using nth_In; vauto. all: try solve [right; split; ins; eauto]. apply In_nth with (d := fl 0) in H; desf; exists n; desf; ins. exists (n + length l); desf; try f_equal; lia. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription