no goals
α : Type u_1
s✝ : HeapNode α
n : Nat
res : Heap α
a : α
c s : HeapNode α
⊢ Heap.realSize (toHeap.go (node a c s) n res) = realSize (node a c s) + Heap.realSize res
simp [toHeap.go, go, Nat.add_assoc, Nat.add_left_comm]