{P : Sort u} →
  {elabs : Array Lean.Elab.Command.InductiveElabStep2} →
    {mctx : Lean.MetavarContext} →
      {levelParams : List Lean.Name} →
        {params : Array Lean.Expr} →
          {lctx : Lean.LocalContext} →
            {localInsts : Lean.LocalInstances} →
              {replaceIndFVars : Lean.Expr → Lean.MetaM Lean.Expr} →
                {elabs' : Array Lean.Elab.Command.InductiveElabStep2} →
                  {mctx' : Lean.MetavarContext} →
                    {levelParams' : List Lean.Name} →
                      {params' : Array Lean.Expr} →
                        {lctx' : Lean.LocalContext} →
                          {localInsts' : Lean.LocalInstances} →
                            {replaceIndFVars' : Lean.Expr → Lean.MetaM Lean.Expr} →
                              { elabs := elabs, mctx := mctx, levelParams := levelParams, params := params,
                                    lctx := lctx, localInsts := localInsts, replaceIndFVars := replaceIndFVars } =
                                  { elabs := elabs', mctx := mctx', levelParams := levelParams', params := params',
                                    lctx := lctx', localInsts := localInsts', replaceIndFVars := replaceIndFVars' } →
                                (elabs = elabs' →
                                    mctx = mctx' →
                                      levelParams = levelParams' →
                                        params = params' →
                                          lctx = lctx' →
                                            localInsts = localInsts' → replaceIndFVars = replaceIndFVars' → P) →
                                  P