{P : Sort u} →
  {knowsType knowsLevel inBottomUp parentIsApp : Bool} →
    {subExpr : Lean.SubExpr} →
      {knowsType' knowsLevel' inBottomUp' parentIsApp' : Bool} →
        {subExpr' : Lean.SubExpr} →
          { knowsType := knowsType, knowsLevel := knowsLevel, inBottomUp := inBottomUp, parentIsApp := parentIsApp,
                subExpr := subExpr } =
              { knowsType := knowsType', knowsLevel := knowsLevel', inBottomUp := inBottomUp',
                parentIsApp := parentIsApp', subExpr := subExpr' } →
            (knowsType = knowsType' →
                knowsLevel = knowsLevel' →
                  inBottomUp = inBottomUp' → parentIsApp = parentIsApp' → subExpr = subExpr' → P) →
              P