theorem Hex.PermGroup.checkWord_spec {n : ℕ} {S : Array (Perm n)} {p : Perm n} {program : Program} (h : checkWord S p program = true) : p.toEquiv ∈ closure S

A successfully replayed word proves membership in Mathlib's subgroup.