proof(coq): add FunctionalExtensionality import to file_operations.v

Consistent with filesystem_model.v — required when extensional equality
of functions is used in subsequent proofs.

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

Author: hyperpolymath

proofs/coq/file_operations.v

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