proposition: Lemma trace_length_map A B (f : A -> B) (t : trace A) : trace_length (trace_map f t) = trace_length t.
proof: Proof. destruct t; ins; eauto using length_map. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription