proposition: Lemma trace_prepend_app A (l l' : list A) fl : trace_prepend (l ++ l') fl = trace_prepend l (trace_prepend l' fl).
proof: Proof. unfold trace_prepend; extensionality n. rewrite length_app, nth_app; desf; try lia. all: first [apply nth_indep | f_equal]; lia. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription