∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α}
  {lhs rhs cin lhs_1 rhs_1 cin_1 : aig.Ref},
  { lhs := lhs, rhs := rhs, cin := cin } = { lhs := lhs_1, rhs := rhs_1, cin := cin_1 } →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ cin = cin_1