proposition: Lemma trace_length_app A (t t' : trace A) : trace_length (trace_app t t') = NOmega.add (trace_length t) (trace_length t').
proof: Proof. destruct t, t'; ins; auto using length_app. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription