| CicUnification.Uncertain _ -> false, menv2, m
in
(* check which "positions" in the input arrow unifies with saturated_ty2 *)
| CicUnification.Uncertain _ -> false, menv2, m
in
(* check which "positions" in the input arrow unifies with saturated_ty2 *)