Type Definition prop::existence::CrossEq

pub type CrossEq<A, B> = And<Imply<A, NN<B>>, Imply<B, NN<A>>>;

a =x= b, defined as (a => ¬¬b) ⋀ (b => ¬¬a).