proposition: Lemma trace_nodup_filter_inj A (f : A -> Prop) t (ND : trace_nodup (trace_filter f t)) n (Ln : NOmega.lt_nat_l n (trace_length t)) m (Lm : NOmega.lt_nat_l m (trace_length t)) d (EQ : trace_nth n t d = trace_nth m t d) (EXT : f (trace_nth n t d)) : n = m.
proof: Proof. assert (Em: f (trace_nth m t d)) by congruence. rewrite <- trace_nth_filter' with (n := m) (f := f) in EQ; ins. rewrite <- trace_nth_filter' with (n := n) (f := f) in EQ; ins; desf. eapply trace_nodup_inj in EQ; ins; try eapply trace_lt_length_filter; eauto. destruct (lt_eq_lt_dec n m) as [[LT|]|LT]; desf. all: rewrite (seq_split0 LT) in *. all: rewrite map_app, filterP_app, length_app in *; ins; desf; ins; lia. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription