∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {m n : ℕ} {target : aig.RefVec m}
  {distance : aig.RefVec n} {n_1 : ℕ} {target_1 : aig.RefVec m} {distance_1 : aig.RefVec n_1},
  { n := n, target := target, distance := distance } = { n := n_1, target := target_1, distance := distance_1 } →
    n = n_1 ∧ target = target_1 ∧ distance ≍ distance_1