∀ {proof : Lean.Expr} {assignment : Array Lean.Expr} {proof_1 : Lean.Expr} {assignment_1 : Array Lean.Expr},
  { proof := proof, assignment := assignment } = { proof := proof_1, assignment := assignment_1 } →
    proof = proof_1 ∧ assignment = assignment_1