∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)}
  {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_1 → Prop} {a : ℕ}
  {a_1 : Std.HashMap α ℕ} (t : Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_1),
  motive 0 ∅ ⋯ →
    (∀ {idx : ℕ} {map : Std.HashMap α ℕ} {a : α} {val : ℕ} (hinv : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map)
        (hlt : idx < decls.size) (hatom : decls[idx] = Std.Sat.AIG.Decl.atom a) (hmap : map[a]? = none),
        motive (idx + 1) (map.insert a val) ⋯) →
      (∀ {idx : ℕ} {map : Std.HashMap α ℕ} {a : α} {n : ℕ} (hinv : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map)
          (hlt : idx < decls.size) (hatom : decls[idx] = Std.Sat.AIG.Decl.atom a) (hmap : map[a]? = some n),
          motive (idx + 1) map ⋯) →
        (∀ {idx : ℕ} {map : Std.HashMap α ℕ} (hinv : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map)
            (hlt : idx < decls.size) (hatom : decls[idx] = Std.Sat.AIG.Decl.false), motive (idx + 1) map ⋯) →
          (∀ {idx : ℕ} {map : Std.HashMap α ℕ} {l r : Std.Sat.AIG.Fanin}
              (hinv : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map) (hlt : idx < decls.size)
              (hatom : decls[idx] = Std.Sat.AIG.Decl.gate l r), motive (idx + 1) map ⋯) →
            motive a a_1 t