+ normalize_machine ~delta ~subst ctx
+ (fst (NCicReduction.reduce_machine ~delta ~subst ctx (0,[],t,[])))
+and normalize_machine ?(delta=0) ~subst ctx (k,e,t,s) =
+ assert (delta=0);
+ let t =
+ if k = 0 then t
+ else
+ NCicSubstitution.psubst ~avoid_beta_redexes:true
+ (fun e -> normalize_machine ~delta ~subst ctx (NCicReduction.from_env ~delta e)) e t in
+ let t =
+ match t with