?1 <= Type_i -->> ?1 := ?2, ?2 : Type_i+1
-nel vecchio nucleo la height_of di un b-redex fa 0 e quindi riduci in forma normale
+nel vecchio nucleo la height_of di un b-redex fa 0 e quindi riduci in forma
+normale. Spostare la small_delta_step.
+
+@ tra universi senza duplicati
-------
?1 = t
(?1,?2)::(?2,t)::subst