induction expr generalizing aig with
| const =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
| literal =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := atomHandler)]
| not expr ih =>
  simp only [go]
  have := go_decls_size_le atomHandler expr aig
  specialize ih aig (by omega) (by omega)
  rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)]
  assumption
| gate g lhs rhs lih rih =>
  have := go_decls_size_le atomHandler lhs aig
  have := go_decls_size_le atomHandler rhs (go lhs aig atomHandler).val.aig
  specialize lih aig (by omega) (by omega)
  specialize rih (go lhs aig atomHandler).val.aig (by omega) (by omega)
  cases g with
  | and =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkAndCached)]
    rw [rih, lih]
  | or =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkOrCached)]
    rw [rih, lih]
  | xor =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkXorCached)]
    rw [rih, lih]
  | beq =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached)]
    rw [rih, lih]
  | imp =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkImpCached)]
    rw [rih, lih]
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
idx : Nat
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr aig atomHandler).val.aig.decls.size
⊢ (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
no goals