proposition: Fact vec_map_fill_tail X Y (f : X -> Y) n k v e : vec_map f (@vec_fill_tail X n k v e) = vec_fill_tail n (vec_map f v) (f e).
proof: Proof. apply vec_pos_ext; intros p; rew vec. destruct (le_lt_dec k (pos2nat p)) as [ | Hp ]. + do 2 (rewrite vec_fill_tail_ge; auto). + do 2 rewrite vec_fill_tail_lt with (Hp := Hp); rew vec. Qed.
imports: List Arith Bool Lia Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic fo_sat)