∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (idx : ℕ)
  (_x :
    (aig : Std.Sat.AIG α) ×'
      (curr : ℕ) ×'
        (_ : curr ≤ w) ×'
          (_ : aig.Ref) ×' (_ : aig.RefVec w) ×' (_ : aig.RefVec w) ×' (_ : aig.RefVec curr) ×' idx < curr)
  (hfoo :
    _x.1.decls.size ≤
      (Std.Sat.AIG.RefVec.ite.go _x.1 _x.2.1 ⋯ _x.2.2.2.1 _x.2.2.2.2.1 _x.2.2.2.2.2.1 _x.2.2.2.2.2.2.1).aig.decls.size),
  (Std.Sat.AIG.RefVec.ite.go _x.1 _x.2.1 ⋯ _x.2.2.2.1 _x.2.2.2.2.1 _x.2.2.2.2.2.1 _x.2.2.2.2.2.2.1).vec.get idx ⋯ =
    (_x.2.2.2.2.2.2.1.get idx ⋯).cast hfoo