. intro h idx hidx
  specialize h idx hidx
  rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)] at h
  rw [← h]
case mp
α : 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

case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
⊢ (∀ (idx : Nat) (hidx : idx < len), ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true) →
    ∀ (idx : Nat) (hidx1 : idx < len),
      ⟦{ aig := (aig.mkConstCached true).aig, ref := { gate := (s.getRef idx hidx1).gate, hgate := ⋯ } }, assign⟧ = true
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
⊢ (∀ (idx : Nat) (hidx : idx < len), ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true) →
    ∀ (idx : Nat) (hidx1 : idx < len),
      ⟦{ aig := (aig.mkConstCached true).aig, ref := { gate := (s.getRef idx hidx1).gate, hgate := ⋯ } }, assign⟧ = true