apply FullAdderOutput.hle
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (mkFullAdder aig input).aig.decls.size
no goals