fact: Definition trace_elems A (t : trace A) := match t with | trace_fin l => (fun a => In a l) | trace_inf fl => (fun a => exists n, a = fl n) end.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription