proposition: Lemma trace_nodup_mapE A B (f : A -> B) (t : trace A) : trace_nodup (trace_map f t) -> trace_nodup t.
proof: Proof. unfold trace_nodup; ins; desf. intro; eapply H; try rewrite trace_length_map; eauto. rewrite !trace_nth_map; eauto using f_equal. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription