Proof engine works internally with normalized terms, clean up

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml