rw [fold.denote_go_and]
α : 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
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
⊢ (⟦{ aig := (aig.mkConstCached true).aig, ref := (aig.mkConstCached true).ref }, assign⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len),
        0 ≤ idx → ⟦{ aig := (aig.mkConstCached true).aig, ref := (s.cast ⋯).getRef idx hidx1 }, assign⟧ = true) ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true

case hcurr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
⊢ 0 ≤ len