proposition: Lemma map_trace_prepend_lt A (l: list A) fl n (LT: n < length l) : exists l' a l'', l = l' ++ a :: l'' /\ length l' = n /\ map (trace_prepend l fl) (List.seq 0 n) = l'.
proof: Proof. unfold trace_prepend. destruct (Nat.le_exists_sub n (length l)) as (p & X & _); try lia. rewrite Nat.add_comm in X. apply length_eq_add in X; desf. rewrite length_app in *; destruct l''; ins; try lia. repeat eexists. eapply map_nth_seq with (d := fl 0); ins; desf; try lia. rewrite nth_app; desf; try lia. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription