fact: Definition trace_filter A (f : A -> Prop) (t : trace A) : trace A := match t with | trace_fin l => trace_fin (filterP f l) | trace_inf fl => let s := excluded_middle_informative (set_finite (set_map fl f)) in match s with | left FIN => let B := set_finite_nat_bounded FIN in let n := proj1_sig (constructive_indefinite_description _ B) in trace_fin (filterP f (map fl (List.seq 0 (S n)))) | right INF => trace_inf (fun n => let H := set_infinite_natE INF n in let H0 := constructive_indefinite_description _ H in fl (proj1_sig H0)) end end.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription