Thm* p,q:. p = q = false p = q beq_neq

In prior sections: core bool 1 int 2 list 1 finite sets list 3 autom exponent rel 1 relation autom action sets det automata