proposition: Lemma trace_elems_filter A (f : A -> Prop) (t : trace A) : trace_elems (trace_filter f t) ≡₁ trace_elems t ∩₁ f.
proof: Proof. repeat autounfold with unfolderDb; split; ins. all: rewrite trace_in_filter in *; desf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription