simplified coercDb implementation with additional info about the position of

simplified coercDb implementation with additional info about the position of
the coerced argument. Now (C ??? x ??? y z) is printed as (x y z) when C is a
coercion and ? are implicits or saturations generated to apply the coercion to
x.

New case in unification, when there is a triangular pullback and the
coerced is not flexible an unfolding of the composed coercion is attempted.
this helps in the case:

  C ??? X ??? y ? +?+ C1 ??? (C2 ??? X ???) ??? y z

where C = C1 composed C2 but X is rigid abd conversion fails cause
x != ? and the heads are different... unfolding C helps