anchor.diff:      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))))
  +            let ty = fst(Choice.get <| 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
  
positive.code:         let _,_,sth =
              assoc tyname (!inductive_type_store)
              |> Option.getOrFailWith "find"
          let ty,zty = dest_fun_ty (Choice.get <| type_of(fst(dest_exists(snd(strip_forall(concl sth))))))
          let rth = INST_TYPE [num_ty,zty] sth
          let avs,bod = strip_forall(concl rth)
          let ev,cbod = dest_exists bod
  
negative.code:         prove_recursive_functions_exist sth (list_mk_conj def)
      let INDUCTIVE_MEASURE_THEN tac (asl,w) =
        let ev,bod = dest_exists w
        let ty = fst(Choice.get <| dest_type(fst(Choice.get <| dest_fun_ty(Choice.get <| type_of ev))))
        let th = prove_depth_measure_exists ty
        let ev',bod' = dest_exists(concl th)
        let th' = INST_TYPE(type_match (Choice.get <| type_of ev') (Choice.get <| type_of ev) []) th
  