apply LawfulOperator.lt_size_of_lt_aig_size (f := mkXorCached)
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.rhs.gate < (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.decls.size
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.rhs.gate < aig.decls.size