proposition: Fact vec_map_list_plus n v w f : @vec_map_list X n (vec_plus v w) f ~p vec_map_list v f ++ vec_map_list w f.
proof: Proof. revert v w f; induction n as [ | n IHn ]; intros v w f. + rewrite (vec_0_nil (vec_plus v w)), (vec_0_nil v), (vec_0_nil w); simpl; auto. + rewrite (vec_head_tail v), (vec_head_tail w), vec_plus_cons. generalize (vec_head v) (vec_tail v) (vec_head w) (vec_tail w); clear v w; intros x v y w. simpl. rewrite list_repeat_plus. solve list eq; apply Permutation_app; auto. apply Permutation_trans with (list_repeat (f pos0) y ++ vec_map_list v (fun p => f (pos_nxt p)) ++ vec_map_list w (fun p => f (pos_nxt p))). * apply Permutation_app; auto. * do 2 rewrite app_assoc. apply Permutation_app; auto. apply Permutation_app_comm. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)