∀ {α : 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} {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),
  Std.Sat.AIG.RelabelNat.State.Inv2.below hinv → motive idx map hinv → Std.Sat.AIG.RelabelNat.State.Inv2.below ⋯