rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls.size
⊢ (aig.mkConstCached (val.getLsb i)).aig.decls[idx] = aig.decls[idx]

case isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls.size
⊢ idx < (aig.mkConstCached (val.getLsb i)).aig.decls.size
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefStream i
val : BitVec w
hi : i ≤ w
res : AIG.RefStreamEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached (val.getLsb i)).aig (i + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (val.getLsb i)).ref) val
            ⋯).aig.decls.size
⊢ idx < (aig.mkConstCached (val.getLsb i)).aig.decls.size