proposition: Lemma trace_prepend_snd A (l: list A) fl n : trace_prepend l fl (length l + n) = fl n.
proof: Proof. unfold trace_prepend; desf; f_equal; lia. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription