proposition: Lemma trace_in_map A (a : A) B (f : B -> A) (t : trace B) : trace_elems (trace_map f t) a <-> exists x, trace_elems t x /\ f x = a.
proof: Proof. destruct t; ins; try rewrite in_map_iff; split; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription