∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (decls : Array (Std.Sat.AIG.Decl α))
  (cache : Std.Sat.AIG.Cache α decls) (hdag : Std.Sat.AIG.IsDAG α decls) (hzero : 0 < decls.size)
  (hconst : decls[0] = Std.Sat.AIG.Decl.false) (decls_1 : Array (Std.Sat.AIG.Decl α))
  (cache_1 : Std.Sat.AIG.Cache α decls_1) (hdag_1 : Std.Sat.AIG.IsDAG α decls_1) (hzero_1 : 0 < decls_1.size)
  (hconst_1 : decls_1[0] = Std.Sat.AIG.Decl.false),
  ({ decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst } =
      { decls := decls_1, cache := cache_1, hdag := hdag_1, hzero := hzero_1, hconst := hconst_1 }) =
    (decls = decls_1 ∧ cache ≍ cache_1)