simp only [denote_projected_entry, mkConstCached_eval_eq_mkConst_eval, denote_mkConst,
Nat.zero_le, getRef_cast, Ref_cast', true_implies, true_and]
α : 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
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
⊢ (∀ (idx : Nat) (hidx1 : idx < len),
      ⟦{ aig := (aig.mkConstCached true).aig, ref := { gate := (s.getRef idx hidx1).gate, hgate := ⋯ } }, assign⟧ =
        true) ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true