rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkAndCached)]
case isTrue.mpr.right
α : 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
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr + 1 ≤ idx
hrest : ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧
case isTrue.mpr.right
α : 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
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr + 1 ≤ idx
hrest : ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ⟦{ aig := aig, ref := { gate := ((input.getRef idx hidx1).cast ⋯).gate, hgate := ?isTrue.mpr.right } }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧

case isTrue.mpr.right
α : 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
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr + 1 ≤ idx
hrest : ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ((input.getRef idx hidx1).cast ⋯).gate < aig.decls.size