Fix go_left_spec
We fix the bug in insert_overflow (See #12 (closed)). There is still a lemma to prove about the new go_left_spec difinition (but now we have defined the unit (soon PBT) to check the equivalence between the specs).
Edited by Germán Delbianco