proofs(idris2): make Filesystem.Model typecheck under Idris2 0.8.0 (#69)

The model used Data.List.lookup, elem, and (==) on values of type Path
and (Path, FSEntry), and called isJust on Maybe values, without bringing
the required Eq instances or the Data.Maybe import into scope. As a
result Filesystem.Model.idr failed to type-check at lines 103/108/135/
152/169, blocking the entire proofs/idris2/ build tree.

Fix the type errors directly:

* Import Data.Maybe so isJust resolves at line 103.
* Add a public-export Eq Path instance defined by structural pattern
  match on the Root/Cons constructors. This sits alongside the existing
  DecEq Path instance and satisfies the Eq constraints required by
  Data.List.lookup, elem, and the Maybe-equality at line 135.
* Add a public-export Eq FSEntry instance matching on Dir/File, which
  satisfies Eq (Path, FSEntry) at line 169 (Idris2 derives Eq on tuples
  from Eq on their components automatically).

No theorems are added or modified. The two ?holes at the bottom of the
file (?equivSymProof, ?equivTransProof) are out of scope for this PR
and remain open — they are tractable separately.

Refs #41 (seam-walk pre-existing failure); unblocks future Idris2
proof work and is a prerequisite for adding a build-idris2 Justfile
target + verify-idris2 CI job (separate follow-up).

Author: hyperpolymath

proofs/idris2/src/Filesystem/Model.idr

@@ -8,6 +8,7 @@
 module Filesystem.Model
 
 import Data.List
+import Data.Maybe
 import Data.String
 import Decidable.Equality
 
@@ -49,6 +50,13 @@ DecEq Path where
     decEq (Cons x xs) (Cons y ys) | No contra =
       No (\Refl => contra Refl)
 
+||| Boolean equality on paths (required by Data.List.lookup / elem)
+public export
+Eq Path where
+  Root         == Root         = True
+  (Cons x xs)  == (Cons y ys)  = x == y && xs == ys
+  _            == _            = False
+
 ||| Parent of a path
 export
 parent : Path -> Maybe Path
@@ -78,6 +86,13 @@ data FSEntry : Type where
   ||| File entry with content
   File : FileContent -> FSEntry
 
+||| Boolean equality on filesystem entries
+public export
+Eq FSEntry where
+  Dir          == Dir          = True
+  (File c1)    == (File c2)    = c1 == c2
+  _            == _            = False
+
 ||| Filesystem state mapping paths to entries
 public export
 record Filesystem where