have := go_decls_size_le atomHandler rhs (go lhs aig atomHandler).val.aig
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]