∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {assign : α → Bool}
  (_x : (aig : Std.Sat.AIG α) ×' (_ : aig.Ref) ×' (curr : ℕ) ×' (_ : curr ≤ len) ×' aig.RefVec len),
  (⟦assign,
        { aig := (Std.Sat.AIG.RefVec.fold.go _x.1 _x.2.1 _x.2.2.1 len _x.2.2.2.2 Std.Sat.AIG.mkAndCached).aig,
          ref := (Std.Sat.AIG.RefVec.fold.go _x.1 _x.2.1 _x.2.2.1 len _x.2.2.2.2 Std.Sat.AIG.mkAndCached).ref }⟧ =
      true) =
    (⟦assign, { aig := _x.1, ref := _x.2.1 }⟧ = true ∧
      ∀ (idx : ℕ) (hidx1 : idx < len),
        _x.2.2.1 ≤ idx → ⟦assign, { aig := _x.1, ref := _x.2.2.2.2.get idx hidx1 }⟧ = true)