proposition: Lemma trace_nth_filter' A (f : A -> Prop) (t : trace A) n d (LT : NOmega.lt_nat_l n (trace_length t)) (F: f (trace_nth n t d)): trace_nth (length (filterP f (map (fun i => trace_nth i t d) (List.seq 0 n)))) (trace_filter f t) d = trace_nth n t d.
proof: Proof. destruct t; ins; desf; ins; eauto using nth_filterP'. { destruct (IndefiniteDescription.constructive_indefinite_description); ins; desf. clear LT; assert (LT := l _ F); ins. rewrite seqS, (seq_split0 LT), appA, map_app, filterP_app. rewrite app_nth2, Nat.sub_diag; ins; desf. } destruct (IndefiniteDescription.constructive_indefinite_description); ins. destruct a as [F' LEQ]. rewrite filterP_map, length_map in *. change (fun i => fl i) with fl in *. clear LT; destruct (lt_eq_lt_dec x n) 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