NOT_EQ_SYM : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Swaps left-hand and right-hand sides of a negated equation.
DESCRIPTION
When applied to a theorem A |- ~(t1 = t2), the inference rule NOT_EQ_SYM returns the theorem A |- ~(t2 = t1). 
    A |- ~(t1 = t2)
   -----------------  NOT_EQ_SYM
    A |- ~(t2 = t1)

FAILURE
Fails unless the theorem’s conclusion is a negated equation.
SEEALSO
DEPTH_CONV, REFL, SYM
HOL  Kananaskis-14