fact: Definition trace_prefix A (t t' : trace A) := match t, t' with | trace_fin l, trace_fin l' => exists l'', l' = l ++ l'' | trace_fin l, trace_inf f => forall i (LLEN: i < length l) d, f i = nth i l d | trace_inf f, trace_fin _ => False | trace_inf f, trace_inf f' => forall x, f x = f' x end.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription