anchor.diff:  /// Defines a general recursive function.
   let define = 
       let close_definition_clauses tm = 
  +        choice {
           let avs, bod = strip_forall tm
           let cjs = conjuncts bod
  -        let fs = 
  -            try 
  -                map (repeat(Choice.toOption << rator) << Choice.get << lhs << snd << strip_forall) cjs
  -            with
  -            | Failure _ -> failwith "close_definition_clauses: non-equation"
  -        if length(setify fs) <> 1 then failwith "close_definition_clauses: defining multiple functions"
  +        let! fs = 
  +            Choice.List.map (Choice.map (repeat(Choice.toOption << rator)) << lhs << snd << strip_forall) cjs
  +            |> Choice.mapError (fun e -> nestedFailure e "close_definition_clauses: non-equation")
  +
  +        if length(setify fs) <> 1 then 
  +            return! Choice.failwith "close_definition_clauses: defining multiple functions"
           else 
               let f = hd fs
  -            if mem f avs then failwith "close_definition_clauses: fn quantified"
  +            if mem f avs then 
  +                return! Choice.failwith "close_definition_clauses: fn quantified"
               else 
                   let do_clause t = 
  +                    choice {
                       let lvs, bod = strip_forall t
  -                    let fvs = subtract (frees(Choice.get <| lhs bod)) (f :: lvs)
  -                    SPECL fvs (ASSUME(list_mk_forall(fvs, t)))
  +                    let! tm1 = lhs bod
  +                    let fvs = subtract (frees tm1) (f :: lvs)
  +                    return! SPECL fvs (ASSUME(list_mk_forall(fvs, t)))
  +                    }
  +
                   let ths = map do_clause cjs
  -                let ajs = map (hd << hyp << Choice.get) ths
  +                let! ajs = Choice.List.map (Choice.map (hd << hyp)) ths
                   let th = ASSUME(list_mk_conj ajs)
  -                f, itlist GEN avs (itlist PROVE_HYP (CONJUNCTS th) (end_itlist CONJ ths))
  +                let! th' = itlist GEN avs (itlist PROVE_HYP (CONJUNCTS th) (end_itlist CONJ ths)) 
  +                return f, th'
  +        }
       fun tm -> 
  -    let tm' = snd(strip_forall tm)
  -    try 
  -        let th, th' = 
  -            tryfind (fun th -> Some(th, PART_MATCH Choice.result th tm')) (!the_definitions) 
  -            |> Option.getOrFailWith "tryfind"
  -        if (Choice.isResult << PART_MATCH Choice.result th')(concl <| Choice.get th) then 
  -            (warn true "Benign redefinition"
  -             th')
  -        else failwith ""
  -    with
  -    | Failure _ -> 
  -        let f, th = close_definition_clauses tm
  -        let etm = Choice.get <| mk_exists(f, hd(hyp <| Choice.get th))
  -        let th1 = prove_general_recursive_function_exists etm
  -        let th2 = new_specification [fst(Choice.get <| dest_var f)] th1
  -        let g = Choice.get <| mk_mconst(Choice.get <| dest_var f)
  -        let th3 = PROVE_HYP th2 (INST [g, f] th)
  -        the_definitions := th3 :: (!the_definitions)
  -        th3
  +        let tm' = snd(strip_forall tm)
  +        choice { 
  +            let! th, th' = 
  +                Choice.List.tryPick (fun th -> 
  +                    choice {
  +                        let! th = th
  +                        let! th' = PART_MATCH Choice.result (Choice.result th) tm' 
  +                        return Some(th, Choice.result th')
  +                    }) (!the_definitions) 
  +                |> Choice.bind (Option.toChoiceWithError "tryfind")
  +            if (Choice.isResult << PART_MATCH Choice.result th')(concl th) then 
  +                warn true "Benign redefinition"
  +                return! th'
  +            else 
  +                return! Choice.failwith ""
  +        }
  +        |> Choice.bindError (function 
  +            | Failure _ -> 
  +                choice {
  +                    let! f, th = close_definition_clauses tm
  +                    let! etm = mk_exists(f, hd(hyp th))
  +                    let th1 = prove_general_recursive_function_exists etm
  +                    let! (s1, _) = dest_var f
  +                    let th2 = new_specification [s1] th1
  +                    let! sht = dest_var f
  +                    let! g = mk_mconst sht
  +                    let th3 = PROVE_HYP th2 (INST [g, f] (Choice.result th))
  +                    the_definitions := th3 :: (!the_definitions)
  +                    return! th3
  +                }
  +            | e -> Choice.error e)
  
positive.code:     | _ -> true in
  
    let MAIN_ADMISS_TAC(asl, w as gl) = 
        let had, args = strip_comb w
        if not(is_const had) then failwith "ADMISS_TAC"
        else 
            let f, fbod = Choice.get <| dest_abs(last args)
            let xtup, bod = Choice.get <| 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", "_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
            | "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 th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN
                (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 th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_GUARDED_PATTERN
                (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
            | "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
            // 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"
      
      in
  
  
negative.code:       let prove_depth_measure_exists = 
            let num_ty = (parse_type @"num")
            fun tyname -> 
              choice {
                let! _, _, sth = assoc tyname (!inductive_type_store) |> Option.toChoiceWithError "find"
                let! sth = sth
                let! (tm1, _) = dest_exists(snd(strip_forall(concl sth)))
                let! ty1 = type_of tm1
                let! ty, zty = dest_fun_ty ty1
                let! rth = INST_TYPE [num_ty, zty] (Choice.result sth)
                let avs, bod = strip_forall(concl rth)
                let! ev, cbod = dest_exists bod
                let process_clause k t = 
                  choice {
                    let avs, eq = strip_forall t
                    let! l, r = dest_eq eq
                    let! fn, cargs = dest_comb l
                    let con, args = strip_comb cargs
                    let! bargs = Choice.List.filter (fun t ->
                                     choice {
                                          let! ty1 = type_of t
                                          return ty1 = 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)
  
                    let! tm2 = mk_eq(l, r')
                    return list_mk_forall(avs, tm1)
                  }
                let cjs = conjuncts cbod
                let! def = Choice.List.map2 process_clause (1 -- length cjs) cjs
                return! prove_recursive_functions_exist (Choice.result sth) (list_mk_conj def)
              }
  
        let INDUCTIVE_MEASURE_THEN tac (asl, w) = 
          choice {
            let! ev, bod = dest_exists w
            let! ty1 = type_of ev
            let! (ty2, _) = dest_fun_ty ty1
            let! (ty, _) = dest_type ty2
            let! th = prove_depth_measure_exists ty
            let! ev', bod' = dest_exists(concl th)
            let! ty3 = type_of ev'
            let! ty4 = type_of ev
            let! ty5 = type_match ty3 ty4 []
            let th' = INST_TYPE ty5 (Choice.result th)
            return!
                (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) -> 
              choice {
                let! ev, bod = dest_exists w
                let! ty1 = type_of ev
                let! (ty, _) = dest_fun_ty ty1
                let! tm1 = mk_abs(genvar ty, one_tm)
  
                return!
                    (EXISTS_TAC tm1
                     |> 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) /\
  