{P : Sort u} →
  {toConstantVal : Lean.ConstantVal} →
    {induct : Lean.Name} →
      {cidx numParams numFields : ℕ} →
        {isUnsafe : Bool} →
          {toConstantVal' : Lean.ConstantVal} →
            {induct' : Lean.Name} →
              {cidx' numParams' numFields' : ℕ} →
                {isUnsafe' : Bool} →
                  { toConstantVal := toConstantVal, induct := induct, cidx := cidx, numParams := numParams,
                        numFields := numFields, isUnsafe := isUnsafe } =
                      { toConstantVal := toConstantVal', induct := induct', cidx := cidx', numParams := numParams',
                        numFields := numFields', isUnsafe := isUnsafe' } →
                    (toConstantVal = toConstantVal' →
                        induct = induct' →
                          cidx = cidx' → numParams = numParams' → numFields = numFields' → isUnsafe = isUnsafe' → P) →
                      P