structure definitions unbundled
Fixed most theorems in basics.v for new structure definitions