proof(coq): replace Axiom functional_extensionality with stdlib import

Remove the hand-rolled Axiom declaration and instead import
Coq.Logic.FunctionalExtensionality. All six Coq proof files
(filesystem_model, file_operations, file_content_operations,
copy_move_operations, symlink_operations, permission_operations,
rmo_operations) use `apply functional_extensionality`; they all
import filesystem_model, so the single import change propagates.

The stdlib version is the standard Coq axiom (fun_ext); this change
makes the axiom dependency explicit and auditable rather than a
locally-declared opaque Axiom.

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

Author: hyperpolymath

proofs/coq/filesystem_model.v

@@ -11,6 +11,7 @@ Require Import String.
 Require Import List.
 Require Import Bool.
 Require Import Arith.
+Require Import Coq.Logic.FunctionalExtensionality.
 Import ListNotations.
 
 (** * Path Model *)
@@ -260,7 +261,5 @@ Proof.
   - assumption.
 Qed.
 
-(** Helper axiom for functional extensionality
-    In real development, import from Coq.Logic.FunctionalExtensionality *)
-Axiom functional_extensionality : forall {A B : Type} (f g : A -> B),
-  (forall x, f x = g x) -> f = g.
+(* functional_extensionality is now provided by
+   Coq.Logic.FunctionalExtensionality (imported above). *)