1. CProp_n fixed to be equal to Type_n to better understand what is happening

1. CProp_n fixed to be equal to Type_n to better understand what is happening
   with universe levels
2. major proof step: I have proved (up to universe inconsistency :-( that
   every RELation induces an OA morphism. In particular, these means:
     A) having correctly defined the four images on subsets
     B) having proved the fundamental symmetry
     C) having proved the two fundamental adjunctions