simp only [FoldTarget.mkAnd]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
⊢ ⟦let res := aig.mkConstCached true;
        let aig_1 := res.aig;
        let acc := res.ref;
        let input := (FoldTarget.mkAnd s).stream.cast ⋯;
        fold.go aig_1 acc 0 (FoldTarget.mkAnd s).len input (FoldTarget.mkAnd s).func,
        assign⟧ =
      true ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
⊢ ⟦fold.go (aig.mkConstCached true).aig (aig.mkConstCached true).ref 0 len (s.cast ⋯) mkAndCached, assign⟧ = true ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true