Very many simplifications

No nz, simplified types, no omega uses (at least now). Thanks to coq
club.