{P : Sort u} →
  {ctors : List Lean.Constructor} →
    {collectUsedFVars : StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit} →
      {checkUniverses : ℕ → Lean.Level → Lean.Elab.TermElabM Unit} →
        {finalizeTermElab : Lean.Elab.TermElabM Unit} →
          {prefinalize :
              List Lean.Name →
                Array Lean.Expr →
                  (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep3} →
            {ctors' : List Lean.Constructor} →
              {collectUsedFVars' : StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit} →
                {checkUniverses' : ℕ → Lean.Level → Lean.Elab.TermElabM Unit} →
                  {finalizeTermElab' : Lean.Elab.TermElabM Unit} →
                    {prefinalize' :
                        List Lean.Name →
                          Array Lean.Expr →
                            (Lean.Expr → Lean.MetaM Lean.Expr) →
                              Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep3} →
                      { ctors := ctors, collectUsedFVars := collectUsedFVars, checkUniverses := checkUniverses,
                            finalizeTermElab := finalizeTermElab, prefinalize := prefinalize } =
                          { ctors := ctors', collectUsedFVars := collectUsedFVars', checkUniverses := checkUniverses',
                            finalizeTermElab := finalizeTermElab', prefinalize := prefinalize' } →
                        (ctors = ctors' →
                            collectUsedFVars = collectUsedFVars' →
                              checkUniverses = checkUniverses' →
                                finalizeTermElab = finalizeTermElab' → prefinalize = prefinalize' → P) →
                          P