proof(SafeGit): DISCHARGE refNameExtracts via Refl (proven#90, #107) (#111)

Per [proven#107](#107)
"overly cautious OWED" pattern.

\`\`\`idris
public export
refNameExtracts : (s : String) -> {auto v : isValidRefName s = True}
               -> refName (MkGitRef s) = s
refNameExtracts _ = Refl
\`\`\`

\`refName\` is a direct pattern match \`refName (MkGitRef name) = name\`
(SafeGit.idr L62-63), so the body reduces by \`Refl\` regardless of
\`s\`. The auto-implicit \`v : isValidRefName s = True\` is irrelevant
to the proof — it's an API precondition on \`s\` that doesn't enter the
reduction.

The OWED's "auto-implicit elaboration" blocker doesn't apply here
because the auto-implicit is just discarded.

Refs #90 #107

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/Proven/SafeGit/Proofs.idr

@@ -31,8 +31,13 @@ forbiddenRefCharsAnchor = Refl
 public export
 0 emptyRefNameInvalid : isValidRefName "" = False
 
-||| OWED: `refName (MkGitRef "main") = "main"` (record extraction
-||| pass-through). Blocked on auto-implicit elaboration.
+||| DISCHARGED: `refName (MkGitRef s) = s` (record extraction
+||| pass-through). `refName` is a direct pattern match
+||| `refName (MkGitRef name) = name` (SafeGit.idr L62-63), so the
+||| body reduces by Refl regardless of `s`. The auto-implicit
+||| `v : isValidRefName s = True` is irrelevant to the proof — it's
+||| an API precondition on `s` that doesn't enter the reduction.
 public export
-0 refNameExtracts : (s : String) -> {auto v : isValidRefName s = True}
-                 -> refName (MkGitRef s) = s
+refNameExtracts : (s : String) -> {auto v : isValidRefName s = True}
+               -> refName (MkGitRef s) = s
+refNameExtracts _ = Refl