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