anchor.diff:      | _ -> true in
   
     let MAIN_ADMISS_TAC(asl, w as gl) = 
  +    choice {
         let had, args = strip_comb w
  -      if not(is_const had) then failwith "ADMISS_TAC"
  +      if not(is_const had) then 
  +          return! Choice.failwith "ADMISS_TAC"
         else 
  -          let f, fbod = Choice.get <| dest_abs(last args)
  -          let xtup, bod = Choice.get <| dest_gabs fbod
  +          let! f, fbod = dest_abs(last args)
  +          let! xtup, bod = dest_gabs fbod
             let hop, args = strip_comb bod
             match (name_of had, name_of hop) with
  -          | "superadmissible", "COND" -> APPLY_PROFORMA_TAC SUPERADMISSIBLE_COND gl
  +          | "superadmissible", "COND" -> 
  +               return! APPLY_PROFORMA_TAC SUPERADMISSIBLE_COND gl
             | "superadmissible", "_MATCH" when name_of(repeat (Choice.toOption << rator) (last args)) = "_SEQPATTERN" -> 
  -              (APPLY_PROFORMA_TAC SUPERADMISSIBLE_MATCH_SEQPATTERN
  -               |> THEN <| CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
  +              return! 
  +                  (APPLY_PROFORMA_TAC SUPERADMISSIBLE_MATCH_SEQPATTERN
  +                   |> THEN <| CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
             | "superadmissible", "_MATCH" when is_pattern "_UNGUARDED_PATTERN" 2 (last args) -> 
  -              let n = length(fst(strip_exists(Choice.get <| body(Choice.get <| body(last args)))))
  +              let! tm1 = body(last args)
  +              let! tm2 = body tm1
  +              let n = length(fst(strip_exists tm2))
                 let th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN
  -              (APPLY_PROFORMA_TAC th
  -               |> THEN <| CONJ_TAC
  -               |> THENL <| [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
  +              return!
  +                  (APPLY_PROFORMA_TAC th
  +                   |> THEN <| CONJ_TAC
  +                   |> THENL <| [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
             | "superadmissible", "_MATCH" when is_pattern "_GUARDED_PATTERN" 3 (last args) -> 
  -              let n = length(fst(strip_exists(Choice.get <| body(Choice.get <| body(last args)))))
  +              let! tm1 = body(last args)
  +              let! tm2 = body tm1
  +              let n = length(fst(strip_exists(tm2)))
                 let th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_GUARDED_PATTERN
  -              (APPLY_PROFORMA_TAC th
  -               |> THEN <| CONJ_TAC
  -               |> THENL <| [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
  +              return!
  +                  (APPLY_PROFORMA_TAC th
  +                   |> THEN <| CONJ_TAC
  +                   |> THENL <| [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
             // Choice.get is safe to use after is_*
             | "superadmissible", _ when is_comb bod && Choice.get <| rator bod = f -> 
  -              APPLY_PROFORMA_TAC SUPERADMISSIBLE_TAIL gl
  -          | "admissible", "sum" -> APPLY_PROFORMA_TAC ADMISSIBLE_SUM gl
  -          | "admissible", "nsum" -> APPLY_PROFORMA_TAC ADMISSIBLE_NSUM gl
  -          | "admissible", "MAP" -> APPLY_PROFORMA_TAC ADMISSIBLE_MAP gl
  +              return! APPLY_PROFORMA_TAC SUPERADMISSIBLE_TAIL gl
  +          | "admissible", "sum" -> 
  +              return! APPLY_PROFORMA_TAC ADMISSIBLE_SUM gl
  +          | "admissible", "nsum" -> 
  +              return! APPLY_PROFORMA_TAC ADMISSIBLE_NSUM gl
  +          | "admissible", "MAP" -> 
  +              return! APPLY_PROFORMA_TAC ADMISSIBLE_MAP gl
             | "admissible", "_MATCH" when name_of(repeat (Choice.toOption << rator) (last args)) = "_SEQPATTERN" -> 
  -              (APPLY_PROFORMA_TAC ADMISSIBLE_MATCH_SEQPATTERN
  -               |> THEN <| CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
  -          | "admissible", "_MATCH" -> APPLY_PROFORMA_TAC ADMISSIBLE_MATCH gl
  -          | "admissible", "_UNGUARDED_PATTERN" -> APPLY_PROFORMA_TAC ADMISSIBLE_UNGUARDED_PATTERN gl
  -          | "admissible", "_GUARDED_PATTERN" -> APPLY_PROFORMA_TAC ADMISSIBLE_GUARDED_PATTERN gl
  -          | "admissible", _ when is_abs bod -> APPLY_PROFORMA_TAC ADMISSIBLE_LAMBDA gl
  +              return!
  +                  (APPLY_PROFORMA_TAC ADMISSIBLE_MATCH_SEQPATTERN
  +                   |> THEN <| CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
  +          | "admissible", "_MATCH" -> 
  +              return! APPLY_PROFORMA_TAC ADMISSIBLE_MATCH gl
  +          | "admissible", "_UNGUARDED_PATTERN" -> 
  +              return! APPLY_PROFORMA_TAC ADMISSIBLE_UNGUARDED_PATTERN gl
  +          | "admissible", "_GUARDED_PATTERN" -> 
  +              return! APPLY_PROFORMA_TAC ADMISSIBLE_GUARDED_PATTERN gl
  +          | "admissible", _ when is_abs bod -> 
  +              return! APPLY_PROFORMA_TAC ADMISSIBLE_LAMBDA gl
             // Choice.get is safe to use after is_*
             | "admissible", _ when is_comb bod && Choice.get <| rator bod = f -> 
  -              if free_in f (Choice.get <| rand bod) then APPLY_PROFORMA_TAC ADMISSIBLE_NEST gl
  -              else APPLY_PROFORMA_TAC ADMISSIBLE_BASE gl
  -          | "admissible", _ when is_comb bod && headonly f bod -> APPLY_PROFORMA_TAC ADMISSIBLE_COMB gl
  -          | _ -> failwith "MAIN_ADMISS_TAC"
  +              if free_in f (Choice.get <| rand bod) then 
  +                  return! APPLY_PROFORMA_TAC ADMISSIBLE_NEST gl
  +              else 
  +                  return! APPLY_PROFORMA_TAC ADMISSIBLE_BASE gl
  +          | "admissible", _ when is_comb bod && headonly f bod -> 
  +               return! APPLY_PROFORMA_TAC ADMISSIBLE_COMB gl
  +          | _ -> 
  +               return! Choice.failwith "MAIN_ADMISS_TAC"
  +    }
       
       in
   
  
positive.code:       let prove_depth_measure_exists = 
            let num_ty = (parse_type @"num")
            fun tyname -> 
            let _, _, sth = assoc tyname (!inductive_type_store) |> Option.getOrFailWith "find"
            let ty, zty = 
                Choice.get 
                <| dest_fun_ty
                       (Choice.get <| type_of(fst(Choice.get <| dest_exists(snd(strip_forall(concl <| Choice.get sth))))))
            let rth = INST_TYPE [num_ty, zty] sth
            let avs, bod = strip_forall(concl <| Choice.get rth)
            let ev, cbod = Choice.get <| dest_exists bod
            let process_clause k t = 
                let avs, eq = strip_forall t
                let l, r = Choice.get <| dest_eq eq
                let fn, cargs = Choice.get <| dest_comb l
                let con, args = strip_comb cargs
                let bargs = filter (fun t -> Choice.get <| type_of t = ty) args
                let r' = 
                    list_mk_binop (parse_term @"(+):num->num->num") 
                        (Choice.get(mk_small_numeral k) :: map (curry (Choice.get << mk_comb) fn) bargs)
                list_mk_forall(avs, Choice.get <| mk_eq(l, r'))
            let cjs = conjuncts cbod
            let def = map2 process_clause (1 -- length cjs) cjs
            prove_recursive_functions_exist sth (list_mk_conj def)
        let INDUCTIVE_MEASURE_THEN tac (asl, w) = 
            let ev, bod = Choice.get <| 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' = Choice.get <| dest_exists(concl <| Choice.get th)
            let th' = INST_TYPE (Choice.get <| type_match (Choice.get <| type_of ev') (Choice.get <| type_of ev) []) th
            (MP_TAC th'
             |> THEN <| MATCH_MP_TAC MONO_EXISTS
             |> THEN <| GEN_TAC
             |> THEN <| DISCH_THEN(fun th -> REWRITE_TAC [th])
             |> THEN <| tac)(asl, w)
        let CONSTANT_MEASURE_THEN = 
            let one_tm = (parse_term @"1")
            fun tac (asl, w) -> 
            let ev, bod = Choice.get <| 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 <| (INDUCTIVE_MEASURE_THEN tac)
            |> ORELSE <| CONSTANT_MEASURE_THEN tac
        let pth_lexleft = 
            prove((parse_term @"(?r. WF(r) /\
                ?s. WF(s) /\
  
negative.code:                                |> THEN <| MATCH_MP_TAC EQ_IMP
                                 |> THEN <| AP_TERM_TAC)
                  |> THEN <| REWRITE_TAC [FUN_EQ_THM; FORALL_PAIR_THM])
  
        let pth_measure = 
            prove((parse_term @"(?m:A->num. P(MEASURE m)) ==> ?r:A->A->bool. WF(r) /\ P r"), MESON_TAC [WF_MEASURE])
  
        let rec GUESS_WF_THEN tac (asl, w) = 
            ((MATCH_MP_TAC pth_lexleft
              |> THEN <| GUESS_WF_THEN(GUESS_WF_THEN tac))
  