fact: Definition trace_app A (t t' : trace A) := match t, t' with | trace_fin l, trace_fin l' => trace_fin (l ++ l') | trace_fin l, trace_inf f => trace_inf (trace_prepend l f) | trace_inf f, _ => trace_inf f end.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription