fix(lean4): remove dead contradiction in nonempty_path_ne_parent

`proofs/lean4/FilesystemModel.lean:97` failed `lake build` under Lean 4.12.0
with "no goals to be solved": the preceding `simp at hp2` derives the
impossible `rest = x :: rest` and closes the goal on its own, so the trailing
`contradiction` was dead code that newer Lean rejects.

Removing it makes `lake build` green again (verified locally with the same
toolchain CI uses — elan -> leanprover/lean4:v4.12.0). This unblocks the
"Verify Lean 4 Proofs" and "Build and Test Lean Extraction Pipeline" CI jobs,
which were pre-existing red on main (not introduced by any recent PR). Only
harmless `unused variable hpre` lints remain; the build succeeds.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU

Author: claude

proofs/lean4/FilesystemModel.lean

@@ -93,8 +93,10 @@ theorem nonempty_path_ne_parent (p : Path) (h : p ≠ []) :
     -- Which means rest = x :: rest (after reverse cancellation), impossible
     have hp2 : p.reverse = x :: rest := hp
     rw [heq] at hp2
+    -- `simp` derives `rest = x :: rest` in `hp2`, which is impossible, so it
+    -- closes the goal on its own; a trailing `contradiction` is dead here
+    -- (Lean 4.12 rejects it as "no goals to be solved").
     simp at hp2
-    contradiction
 
 theorem pathExists_emptyFS_root :
     pathExists rootPath emptyFS := by