+ if not (eta_eq t2 u2) then begin\r
+ let is_relevant = function `Some b -> !b | _ -> false in\r
+ if not (is_relevant b1 || is_relevant b2) then begin\r
+ print_string "WARNING! Stepping on a useless argument!";\r
+print_string (string_of_t t ^ " <==> " ^ string_of_t u);\r
+ ignore(read_line())\r
+ end ;\r
+ Some (k-1)\r
+ end\r