proof(coq): add FunctionalExtensionality import to copy_move + symlink ops

Consistent import across all Coq proof files that transitively use
functional extensionality via filesystem_model.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

proofs/coq/copy_move_operations.v

@@ -15,6 +15,8 @@ Require Import Bool.
 Require Import Arith.
 Import ListNotations.
 
+Require Import Coq.Logic.FunctionalExtensionality.
+
 (* Import base filesystem model *)
 Require Import filesystem_model.
 Require Import file_operations.

proofs/coq/symlink_operations.v

@@ -9,6 +9,8 @@ Require Import String.
 Require Import List.
 Import ListNotations.
 
+Require Import Coq.Logic.FunctionalExtensionality.
+
 Require Import filesystem_model.
 
 (** * Symlink Operations *)