{P : Sort u} →
  {proof : Lean.Expr} →
    {assignment : Array Lean.Expr} →
      {proof' : Lean.Expr} →
        {assignment' : Array Lean.Expr} →
          { proof := proof, assignment := assignment } = { proof := proof', assignment := assignment' } →
            (proof = proof' → assignment = assignment' → P) → P