proposition: Fact vec_first_half_fill_tail v e : vec_first_half (vec_fill_tail _ v e) = v.
proof: Proof. apply vec_pos_ext; intros p. unfold vec_first_half; rew vec. match goal with | |- vec_pos _ ?p = _ => assert (H : pos2nat p < k) end. { rewrite pos2nat_nat2pos; apply pos2nat_prop. } rewrite vec_fill_tail_lt with (Hp := H). revert H. rewrite pos2nat_nat2pos. intros; f_equal; apply nat2pos_pos2nat. 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)