Fix quantifiers and propagation of equality in fourier

See merge request bobot/colibrics!3

Some extensions

See merge request bobot/colibrics!2

  allows to do the twowatchliteral during enqueue

Two watch literal not needed, since the must be all set

Iterative deepening must limit the depth

See merge request bobot/colibrics!1

 And fix generation of ADT

    And check the model before sat

 Remains a todo with type substitution

    - Handle a little of floor and ceil as (- (floor (- x)))

    - But in order to be really useful in fourier factorization is needed

  - perhaps less efficient but normalization can also be used
  - allows to remove CC terms from parents information
  - separately fix a missing find_def in fourier

  - deduce only contradiction

 - handle all the lasteffort of the same time at the same time
 - Handle coercion in Arith

  Quantifiers instantiate not eager triggers during LastEffort