The mvcgen' tactic, split across the modules above.

• VCGen.Reduce — SymM head-redex reducer.
• VCGen.SpecDB — SpecTheoremNew/SpecTheoremsNew + database operations.
• VCGen.RuleConstruction — SymM rule constructors from spec/simp/split info.
• VCGen.Context — VCGenM, its Context/State, the bundle of pre-built rules.
• VCGen.Util — generic VCGenM helpers (introsSimp, repeatAndRfl, app builders).
• VCGen.RuleCache — VCGenM cache wrappers around the SymM rule constructors.
• VCGen.Entails — entailment-shaped goal decomposition (solveSPredEntails etc.).
• VCGen.Solve — the main solve step / SolveResult.
• VCGen.Driver — the worklist driver (work, emitVC, main, Result).
• VCGen.Frontend — the mvcgen' syntax + tactic elaborator + mkSpecContext.