rw [rih, lih]
case gate.xor
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < 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
hbounds : idx < (go (BoolExpr.gate Gate.xor lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.xor.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < 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
hbounds : idx < (go (BoolExpr.gate Gate.xor lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size
no goals