fact: Definition trace_prepend A (l : list A) (fl : nat -> A) n := if Nat.ltb n (length l) then nth n l (fl 0) else fl (n - length l).
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription