Constructor dispatch for copy-on-write overlays

This module is the acyclic assembly point for the individual overlay constructor proofs. It exposes the single strong-induction step consumed by the final mutual scheduler.

theorem IndexedGrammar.Aho.overlayScheduleRun_of_smaller {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) (ordinaryIH : ∀ {B : g.nt} {residualStack : List g.flag} {v : List T} (q : g.NFParse B residualStack v), q.nodeCount < parse.nodeCount → OrdinaryScheduleRuns q) (overlayIH : ∀ {B : g.nt} {residualStack : List g.flag} {v : List T} (q : g.NFParse B residualStack v), q.nodeCount < parse.nodeCount → OverlayScheduleRun q) : OverlayScheduleRun parse

Complete overlay-mode constructor dispatch under the mutual strong-induction hypotheses.