proposition: Lemma trace_in_filter A (a : A) (f : A -> Prop) (t : trace A) : trace_elems (trace_filter f t) a <-> trace_elems t a /\ f a.
proof: Proof. destruct t; ins; desf; ins; rewrite ?in_filterP_iff, ?in_map_iff; ins. all: split; ins; desf; splits; eauto. all: try (eexists; try split; ins). all: destruct (constructive_indefinite_description); ins; desf. { in_simp; apply l in H0; lia. } revert a0. instantiate (1 := length (filterP (fl ↓₁ f) (List.seq 0 n0))). destruct (lt_eq_lt_dec x n0) as [[LT|]|LT]; desf. unfold set_map. all: rewrite (seq_split0 LT), filterP_app, length_app; ins; desf; ins; lia. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription