. simp only [denote_projected_entry, mkConstCached_eval_eq_mkConst_eval, denote_mkConst,
  Nat.zero_le, getRef_cast, Ref_cast', true_implies, true_and]
  constructor
  . intro h idx hidx
    specialize h idx hidx
    rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)] at h
    rw [← h]
  . intro h idx hidx
    specialize h idx hidx
    rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    . simp only [← h]
    . apply RefStream.hrefs
      simp [FoldTarget.mkAnd, hidx]
α : 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
case hcurr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
⊢ 0 ≤ len