Description: Conjunction distributes over exclusive-or. In intuitionistic logic this
assertion is also true, even though xordi does not necessarily hold, in
part because the usual definition of xor is subtly different in
intuitionistic logic. (Contributed by David A. Wheeler, 7-Oct-2018)