proof(coq): add FunctionalExtensionality import to remaining ops files

Complete the import sweep: file_content_operations.v, permission_operations.v.
All Coq proof files now consistently import FunctionalExtensionality.

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

Author: hyperpolymath

proofs/coq/file_content_operations.v

@@ -13,6 +13,8 @@ Require Import List.
 Require Import Bool.
 Import ListNotations.
 
+Require Import Coq.Logic.FunctionalExtensionality.
+
 Require Import filesystem_model.
 Require Import file_operations.
 

proofs/coq/permission_operations.v

@@ -12,6 +12,8 @@ Require Import Bool.
 Require Import Arith.
 Import ListNotations.
 
+Require Import Coq.Logic.FunctionalExtensionality.
+
 Require Import filesystem_model.
 
 (** * Extended Types for Permission/Ownership *)