. simp only [denote_projected_entry, denote_mkAndCached, Bool.and_eq_true, getRef_cast,
    eq_iff_iff]
  constructor
  . intro h
    rcases h with ⟨⟨h1, h2⟩, h3⟩
    constructor
    . assumption
    . intro idx hidx1 hidx2
      cases Nat.eq_or_lt_of_le hidx2 with
      | inl heq => simpa [heq] using h2
      | inr hlt =>
        specialize h3 idx hidx1 (by omega)
        rw [← h3]
        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkAndCached)]
        . simp
        . simp [Ref.hgate]
  . simp only [and_imp]
    intro hacc hrest
    constructor
    . simp [hacc, hrest]
    . intro idx hidx1 hidx2
      specialize hrest idx hidx1 (by omega)
      rw [← hrest]
      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkAndCached)]
      . simp
      . simp [Ref.hgate]
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ (⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
            ref := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref },
          assign⟧ =
        true ∧
      ∀ (idx : Nat) (hidx1 : idx < len),
        curr + 1 ≤ idx →
          ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
                ref := (input.cast ⋯).getRef idx hidx1 },
              assign⟧ =
            true) =
    (⟦{ aig := aig, ref := acc }, assign⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true)

case isTrue.hcurr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ curr + 1 ≤ len
case isTrue.hcurr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ curr + 1 ≤ len