anchor.diff:        TOP_DEPTH_CONV GEN_BETA_CONV
       let tuple_function_existence tm =
         let f,def = dest_exists tm
  -      let domtys0,ranty0 = splitlist dest_fun_ty (Choice.get <| type_of f)
  +      let domtys0,ranty0 = splitlist (Choice.get << dest_fun_ty) (Choice.get <| type_of f)
         let nargs =
           itlist
            (max << length << snd << strip_comb << lhs << snd << strip_forall)
  
positive.code:     let GUESS_ORDERING_TAC =
        let false_tm = (parse_term @"\x:A y:A. F")
        W(fun (asl,w) ->
              let ty = fst(dest_fun_ty(Choice.get <| type_of(fst(dest_exists w))))
              EXISTS_TAC(Choice.get <| inst [ty,aty] false_tm) |>THEN<|
              REWRITE_TAC[WF_FALSE] |>THEN<| NO_TAC) |>ORELSE<|
        GUESS_WF_THEN
  
negative.code:       let one_tm = (parse_term @"1")
        fun tac (asl,w) ->
          let ev,bod = dest_exists w
          let ty = fst(Choice.get <| dest_fun_ty(Choice.get <| type_of ev))
          (EXISTS_TAC(Choice.get <| mk_abs(genvar ty,one_tm)) |>THEN<| tac) (asl,w)
      let GUESS_MEASURE_THEN tac =
        (EXISTS_TAC (parse_term @"\n. n + 1") |>THEN<| tac) |>ORELSE<|
  