fix(ci): make the Coq gate actually run in the pinned container

First CI run failed with `coqc: not found`. Two distinct causes, both
reproduced locally against the digest-pinned image with podman:

1. The coqorg images install Coq into an opam switch owned by the `coq` user
   and put it on PATH via an ENTRYPOINT wrapper. GitHub Actions overrides the
   entrypoint for job containers, so the wrapper never runs and `coqc` is not
   on PATH. Now resolved explicitly, globbed rather than hard-coded so an image
   bump cannot silently break it, and failing loudly if it cannot be found.

2. GitHub fell back to `sh -e {0}` (dash) rather than bash, which rejects
   `set -o pipefail` and the bash-only string operations the gate uses. The
   image does ship bash 5.2, so the shell is now declared explicitly instead
   of depending on the runner's detection.

Verified by running the gate's exact logic inside the pinned image under bash:
prover 8.20.1, 20/20 proofs checked, completeness guard passes, no axioms.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/coq-proof-gate.yml

@@ -28,6 +28,13 @@ jobs:
   coq-proofs:
     runs-on: ubuntu-latest
     timeout-minutes: 30
+    # The image ships bash 5.2, but GitHub fell back to `sh -e {0}` (dash) on
+    # the first run, which rejects `set -o pipefail` and the bash-only string
+    # operations below. Declare the shell explicitly rather than depending on
+    # the runner's detection.
+    defaults:
+      run:
+        shell: bash
     container:
       # coqorg/coq:8.20 — pinned by digest. `formal/README.adoc` documents 8.18;
       # the corpus was verified to check clean on 8.20.1 (deprecation warnings
@@ -37,6 +44,23 @@ jobs:
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
 
+      # The coqorg images install Coq into an opam switch owned by the `coq`
+      # user and put it on PATH via an ENTRYPOINT wrapper. GitHub Actions
+      # overrides the entrypoint for job containers, so that wrapper never
+      # runs and `coqc` is not on PATH — the switch has to be added by hand.
+      # Globbed rather than hard-coded so an image bump does not silently
+      # break the gate; fails loudly if the switch cannot be located.
+      - name: Put the image's opam switch on PATH
+        run: |
+          set -euo pipefail
+          sw="$(ls -d /home/coq/.opam/*/bin 2>/dev/null | head -1 || true)"
+          if [ -z "$sw" ] || [ ! -x "$sw/coqc" ]; then
+            echo "::error::could not locate coqc in the image's opam switch"
+            exit 1
+          fi
+          echo "$sw" >> "$GITHUB_PATH"
+          echo "added $sw to PATH"
+
       - name: Record prover version
         run: coqc --version