{P : Sort u} →
  {ppExprWithInfos : Lean.PPContext → Lean.Expr → IO Lean.FormatWithInfos} →
    {ppConstNameWithInfos : Lean.PPContext → Lean.Name → IO Lean.FormatWithInfos} →
      {ppTerm : Lean.PPContext → Lean.Term → IO Std.Format} →
        {ppLevel : Lean.PPContext → Lean.Level → BaseIO Std.Format} →
          {ppGoal : Lean.PPContext → Lean.MVarId → IO Std.Format} →
            {ppExprWithInfos' : Lean.PPContext → Lean.Expr → IO Lean.FormatWithInfos} →
              {ppConstNameWithInfos' : Lean.PPContext → Lean.Name → IO Lean.FormatWithInfos} →
                {ppTerm' : Lean.PPContext → Lean.Term → IO Std.Format} →
                  {ppLevel' : Lean.PPContext → Lean.Level → BaseIO Std.Format} →
                    {ppGoal' : Lean.PPContext → Lean.MVarId → IO Std.Format} →
                      { ppExprWithInfos := ppExprWithInfos, ppConstNameWithInfos := ppConstNameWithInfos,
                            ppTerm := ppTerm, ppLevel := ppLevel, ppGoal := ppGoal } =
                          { ppExprWithInfos := ppExprWithInfos', ppConstNameWithInfos := ppConstNameWithInfos',
                            ppTerm := ppTerm', ppLevel := ppLevel', ppGoal := ppGoal' } →
                        (ppExprWithInfos = ppExprWithInfos' →
                            ppConstNameWithInfos = ppConstNameWithInfos' →
                              ppTerm = ppTerm' → ppLevel = ppLevel' → ppGoal = ppGoal' → P) →
                          P