Refactoring
New module for automatic conversion

  Basic functions
  Error messages
  Simple example
Added support for Forall and Property automatic conversion
Added more tests with new features not yet supported
Refactoring
Modular approach to conversion for special constructs

  Issues
  1) Non termination (mutual recursion)
  2) Carrying around support proof
Added functions to handle special constructors

  Unfortunately even if supportedSpecial and convertSpecial
  are defined similarly, absurd patterns are rejected
Better formulation for support and conversion of special constructs

  The type List (Arg Term) is a rather nested data type.
  Using simple pattern match does not work out well because
  the checker is not clever enough to realize complete case
  analysis or absurd patterns.
  Thus, instaed of listing the numerous cases, it's more clear
  to pattern match on the data types one at the time
Tested Not
Added support for Or
Added support for Exists

  At the moment the test is not working due to an incomplete pattern matching
  that unfortunately it's not shown
The actual conversion works (test5')

  The incomplete pattern match is in support
  but it seems complete to me.
  Also lemma5 (which contains ∃) is an example of a
  lemma that doesn't live in Set 0 (it's actually Set1), but we still would
  like to convert.
  After quoting the actual sort is unknown (probably due to ⊔).
Removed any check on the sort of a type for automatic conversion

  - Fixed test5
Added And constructor
Refactoring

  Removed computeBListTree as this information can be inferred.
Refactoring
Refactoring
Merge branch 'auto-conv-modular'

Conflicts:
	src/Base.agda
Refactoring