∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} (n : ℕ) (lhs : aig.RefVec w)
  (rhs : aig.RefVec n) (pow n_1 : ℕ) (lhs_1 : aig.RefVec w) (rhs_1 : aig.RefVec n_1) (pow_1 : ℕ),
  ({ n := n, lhs := lhs, rhs := rhs, pow := pow } = { n := n_1, lhs := lhs_1, rhs := rhs_1, pow := pow_1 }) =
    (n = n_1 ∧ lhs = lhs_1 ∧ rhs ≍ rhs_1 ∧ pow = pow_1)