minor reorganisation
more reorganisation, generic simplification for binary boolean ops
work towards proving hyps for ! and ? at arbitrary types

not quite working yet. also apparently need something for =.