Nonstandard connectives of intuitionistic propositional logic.
Michael Kaminski · Notre Dame Journal of Formal Logic · 1988
that must be valid in any reasonable semantics is not provable in LJ\! {A = B denotes {A D B) Λ {B D A)).Moreover, it is not hard to show that the following natural rule of inference does not hold in LJ\