?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.
-------
?1 = t