theorem Hex.PermGroup.Group.word?_spec {n : ℕ} (G : Group n) (p : Perm n) : (∃ (w : Program), G.word? p = some w ∧ checkWord G.generators p w = true) ↔ p.toEquiv ∈ closure G.generators

Membership programs exist exactly for the corresponding Mathlib subgroup.

theorem Hex.PermGroup.Group.subgroupWords?_spec {n : ℕ} (H G : Group n) : (H.subgroupWords? G).isSome = true ↔ closure H.generators ≤ closure G.generators

Containment certificates decide inclusion of the corresponding subgroups.