proposition: Lemma trace_nodup_filter A (f : A -> Prop) (t : trace A) : trace_nodup t -> trace_nodup (trace_filter f t).
proof: Proof. unfold trace_nodup; ins; desf. red; intros. forward eapply trace_nth_filter with (i := i) (d := d) as (n & LTn & N); eauto with hahn. forward eapply trace_nth_filter with (i := j) (d := d) as (m & LTm & M); eauto with hahn. desf. destruct (lt_eq_lt_dec n m) as [[LT|]|LT]; desf; try lia; eapply H with (d := d) in LT; congruence. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription