The Reasoning Operators ⇒ and ⇔

`rArr` and `hArr` are not propositional operators

• different syntax:
  `(2x-6 = 0 harr 2x = 6) harr x = 3` is the same as
    `2x-6 = 0 harr 2x = 6 harr x = 3`
  `(2x-6 = 0 hArr 2x = 6) hArr x = 3` is a syntax error
  verbose_off ok_text You see! modulo 13 (2x-6 = 0 <-> 2x = 6) <-> x = 3 /**/<=> 2x-6 = 0 <-> 2x = 6 <-> x = 3 /**/<=> x=3
  verbose_off ok_text You changed something! modulo 13 (2x-6 = 0 <=> 2x = 6) <=> x = 3
  verbose_off ok_text You changed something! tree_compare 2x-6 = 0 <-> 2x = 6 <-> x = 3; 2x-6 = 0 <=> 2x = 6 <=> x = 3
• so negation cannot be applied to `rArr` and `hArr`
   
• different meaning of chains:
  `2x-6 = 0 hArr 2x = 6 hArr x = 3` is valid for every `x in RR`
  `2x-6 = 0 harr 2x = 6 harr x = 3` yields F when `x ne 3`
   
• different reaction to context information
  case `x < 0`: … `x^2 = 9 hArr x = -3`

• `sqrt(x) = 2 hArr x=4` yields it when `x = -1`

  `rArr`	F	U	T		`hArr`	F	U	T
  F	✓	✓	✓		F	✓	✓	–
  U	✓	✓	✓		U	✓	✓	–
  T	–	–	✓		T	–	–	✓