proposition: Lemma trace_nth_filter A (f : A -> Prop) (t : trace A) i d (LT : NOmega.lt_nat_l i (trace_length (trace_filter f t))) : exists n, NOmega.lt_nat_l n (trace_length t) /\ trace_nth i (trace_filter f t) d = trace_nth n t d /\ i = length (filterP f (map (fun i => trace_nth i t d) (List.seq 0 n))).
proof: Proof. destruct t; ins; desf; ins. { apply nth_filterP; ins. } { destruct (IndefiniteDescription.constructive_indefinite_description); ins; desf. apply nth_filterP with (d := d) in LT; desf. rewrite map_length, seq_length in *; ins. exists n; splits; try rewrite map_length, seq_length; ins. rewrite LT0, nth_indep with (d' := fl 0); ins. rewrite map_nth, seq_nth; ins. rewrite map_length, seq_length; ins. do 2 f_equal; apply map_ext_in; ins; in_simp. rewrite nth_indep with (d' := fl 0); ins. rewrite map_nth, seq_nth; ins; lia. rewrite map_length, seq_length; ins; lia. } destruct set_infinite_natE with (n := i) as (m & F & NF). exists m; desf. destruct (IndefiniteDescription.constructive_indefinite_description); ins; desf. rewrite filterP_map, length_map; splits; ins. clear LT; destruct (lt_eq_lt_dec x m) as [[LT|]|LT]; desf. all: rewrite (seq_split0 LT), filterP_app, length_app in *; ins; desf; ins; lia. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription