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