Updated Test.Convert for last changes in the reflection module
Fixed conversion of not

  ¬ A is normalized now to A -> ⊥ , which is a pi construct when quoted.
[Red] Major changes in the conversion process

  Simplified conversion with a new definition of Special

  Since terms are normalized and eta-converted it seems impossible to distinguish
  ∃ from ×.
Handled correctly existential constructs

  More examples and tests
Added ad-hoc definition of pair in Converter

  Fixed example of conversion using this one.
Merge branch 'porting2.4.2' into generator
Refactoring
Used postulates for lemmas in Converter examples
Refactoring of old example set