NB. TODO check order swap
 
x~y ==> y :~ x
x:~y ==> f x :~ f y
f:~g ==> f x :~ g x
x :~ NotYet
x :~ x
y :~ z ==> x,y :~ x,z
x :~ a && y :~ b ==> (x|y) :~ (a & b) && (x&y) :~ (a|b)