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

Thm* p,q:. p = q = true p = q beq_eq

Thm* p,q:. p = q = q = p beq_sym

Thm* p:. p = p = true beq_id