bool 1 Doc

Def p=q == (pq) (pq)

Thm* assert_of_eq_bool