fact: Definition trace_nth (n : nat) A (t : trace A) (d : A) : A := match t with | trace_fin l => nth n l d | trace_inf fl => fl n end.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription