Changed derivation of repeated quotient to pointwise check. Next: Documentation and chopping down into theories. Need to fix normal DHOL w/ subtypes on-the-fly.

The translation of definitions still fails when the type of definiens cannot be inferred (correctly) in that case no definition is generated