proposition: Lemma set_finite_prepend A (l : list A) (fl : nat -> A) (f : A -> Prop) : set_finite (set_map (trace_prepend l fl) f) <-> set_finite (set_map fl f).
proof: Proof. unfold trace_prepend, set_finite, set_map. split; ins; desf. { exists (map (fun x => x - length l) findom); intro y; ins. rewrite in_map_iff. specialize (H (y + length l)); desf; eauto; try lia. exists (y + length l); rewrite Nat.add_sub in *; eauto. } { exists (List.seq 0 (length l) ++ map (fun x => x + length l) findom); intro y; ins. rewrite in_app_iff, in_seq0_iff, in_map_iff; desf; eauto. apply H in IN. right; eexists; split; eauto; lia. } Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription