∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (motive : Std.Sat.AIG α → Sort u_1)
  (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)
  (h_1 :
    (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) →
              motive { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }),
  (match { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst } with
    | { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst } =>
      h_1 decls cache hdag hzero hconst) =
    h_1 decls cache hdag hzero hconst