simp [addWithCarry, addWithCarry_negate (H := H)]
H : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
⊢ addWithCarry (node l✝ r✝) (negate (node l✝ r✝)) 1 = (1, ofNat (() :: H) 0)
no goals