. dsimp at hgo
  rw [← hgo]
  rw [denote_go_and]
  . 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]
  . omega
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 :
  (let res := aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ };
    let aig_1 := res.aig;
    let newAcc := res.ref;
    let input := input.cast ⋯;
    go aig_1 newAcc (curr + 1) len input mkAndCached) =
    res
⊢ (⟦{ aig := res.aig, ref := res.ref }, 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 isFalse
α : 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 : { aig := aig, ref := acc } = res
⊢ (⟦{ aig := res.aig, ref := res.ref }, 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 isFalse
α : 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 : { aig := aig, ref := acc } = res
⊢ (⟦{ aig := res.aig, ref := res.ref }, assign⟧ = true) =
    (⟦{ aig := aig, ref := acc }, assign⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true)