Original overflowing implementation of singleton insert
Implements #4 (closed)
TODO
-
Prove insert_pow specification -
Clear admitted overflow axiom in insert_overflow.v -
Pack Specification
Edited by Germán Delbianco
Implements #4 (closed)
TODO