(* Takes a well-typed term and *)
(* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
(* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
-(* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
+(* w.r.t. zero or more variables and if the Fix can be reductaed, than it *)
(* is reduced, the delta-reduction is succesfull and the whole algorithm *)
(* is applied again to the new redex; Step 3) is applied to the result *)
(* of the recursive simplification. Otherwise, if the Fix can not be *)