proposition: Lemma trace_elems_map A B (f : B -> A) (t : trace B) : trace_elems (trace_map f t) ≡₁ set_collect f (trace_elems t).
proof: Proof. unfold set_collect; split; intro x; destruct t; ins; desf; try rewrite in_map_iff in *; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription