fact: Definition trace_length A (t : trace A) : nat_omega := match t with | trace_fin l => NOnum (length l) | trace_inf fl => NOinfinity end.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription