∀ {α : Type u} {inst : AddMonoid α} {val neg : α} {val_neg : val + neg = 0} {neg_val : neg + val = 0} {val_1 neg_1 : α}
  {val_neg_1 : val_1 + neg_1 = 0} {neg_val_1 : neg_1 + val_1 = 0},
  { val := val, neg := neg, val_neg := val_neg, neg_val := neg_val } =
      { val := val_1, neg := neg_1, val_neg := val_neg_1, neg_val := neg_val_1 } →
    val = val_1 ∧ neg = neg_1