∀ {symm : Bool} {proof replacement : Lean.Expr} {stringLength : ℕ} {extraGoals : Array (Lean.MVarId × Lean.BinderInfo)}
  {makesNewMVars symm_1 : Bool} {proof_1 replacement_1 : Lean.Expr} {stringLength_1 : ℕ}
  {extraGoals_1 : Array (Lean.MVarId × Lean.BinderInfo)} {makesNewMVars_1 : Bool},
  { symm := symm, proof := proof, replacement := replacement, stringLength := stringLength, extraGoals := extraGoals,
        makesNewMVars := makesNewMVars } =
      { symm := symm_1, proof := proof_1, replacement := replacement_1, stringLength := stringLength_1,
        extraGoals := extraGoals_1, makesNewMVars := makesNewMVars_1 } →
    symm = symm_1 ∧
      proof = proof_1 ∧
        replacement = replacement_1 ∧
          stringLength = stringLength_1 ∧ extraGoals = extraGoals_1 ∧ makesNewMVars = makesNewMVars_1