anchor.diff:            let conv0 = REWR_CONV pth0
             let conv1 = REWR_CONV pth1
             let rec conv tm = 
  -              try 
  -                  conv0 tm
  -              with
  -              | Failure _ -> 
  -                  let th = conv1 tm
  -                  CONV_RULE (funpow 2 RAND_CONV conv) th
  +              conv0 tm
  +              |> Choice.bindError (function
  +                    | Failure _ -> 
  +                          let th = conv1 tm
  +                          CONV_RULE (funpow 2 RAND_CONV conv) th
  +                    | e -> Choice.error e)
             conv
         let LAMBDA_PAIR_CONV = 
  +        
             let rewr1 = GEN_REWRITE_RULE I [GSYM FORALL_PAIR_THM]
             let rewr2 = GEN_REWRITE_CONV I [FUN_EQ_THM]
             fun parms tm -> 
  -          let parm = end_itlist (curry(Choice.get << mk_pair)) parms
  -          let x, bod = Choice.get <| dest_abs tm
  -          let tm' = Choice.get <| mk_gabs(parm, Choice.get <| vsubst [parm, x] bod)
  -          let th1 = BETA_CONV(Choice.get <| mk_comb(tm, parm))
  -          let th2 = GEN_BETA_CONV(Choice.get <| mk_comb(tm', parm))
  -          let th3 = TRANS th1 (SYM th2)
  -          let th4 = itlist (fun v th -> rewr1(GEN v th)) (butlast parms) (GEN (last parms) th3)
  -          EQ_MP (SYM(rewr2(Choice.get <| mk_eq(tm, tm')))) th4
  +            choice {
  +              let parm = end_itlist (curry (Choice.get << mk_pair)) parms
  +              let! x, bod = dest_abs tm
  +              let! tm1 = vsubst [parm, x] bod
  +              let! tm' = mk_gabs(parm, tm1)
  +              let! tm2 = mk_comb(tm, parm)
  +              let th1 = BETA_CONV tm2
  +              let! tm3 = mk_comb(tm', parm)
  +              let th2 = GEN_BETA_CONV tm3
  +              let th3 = TRANS th1 (SYM th2)
  +              let th4 = itlist (fun v th -> rewr1(GEN v th)) (butlast parms) (GEN (last parms) th3)
  +              let! tm4 = mk_eq(tm, tm')
  +              return! EQ_MP (SYM(rewr2 tm4)) th4
  +            }
  +
         let FORALL_PAIR_CONV = 
             let rule = GEN_REWRITE_RULE RAND_CONV [GSYM FORALL_PAIR_THM]
             let rec depair l t = 
                 match l with
                 | [v] -> REFL t
                 | v :: vs -> rule(BINDER_CONV (depair vs) t)
  -              | [] -> failwith "depair: Unhandled case."
  +              | [] -> Choice.failwith "depair: Unhandled case."
  +
             fun parm parms -> 
  -          let p = mk_var("P", Choice.get <| mk_fun_ty (Choice.get <| type_of parm) bool_ty)
  -          let tm = list_mk_forall(parms, Choice.get <| mk_comb(p, parm))
  -          GEN p (SYM(depair parms tm))
  +              let p = mk_var("P", Choice.get <| mk_fun_ty (Choice.get <| type_of parm) bool_ty)
  +              let tm = list_mk_forall(parms, Choice.get <| mk_comb(p, parm))
  +              GEN p (SYM(depair parms tm))
  +
         let ELIM_LISTOPS_CONV = 
             PURE_REWRITE_CONV [PAIRWISE;
                                ALL;
                                GSYM CONJ_ASSOC;
                                AND_CLAUSES]
             |> THENC <| TOP_DEPTH_CONV GEN_BETA_CONV
  +
         let tuple_function_existence tm = 
  -          let f, def = Choice.get <| dest_exists tm
  -          let domtys0, ranty0 = splitlist (Choice.toOption << dest_fun_ty) (Choice.get <| type_of f)
  +        choice {
  +          let! f, def = dest_exists tm
  +          let! ty1 = type_of f
  +          let domtys0, ranty0 = splitlist (Choice.toOption << dest_fun_ty) ty1
             let nargs = 
                 itlist (max << length << snd << strip_comb << Choice.get << lhs << snd << strip_forall) 
                     (conjuncts(snd(strip_forall def))) 0
  +
             let domtys, midtys = chop_list nargs domtys0
  -          let ranty = itlist (fun ty -> Choice.get << mk_fun_ty ty) midtys ranty0
  -          if length domtys <= 1 then ASSUME tm
  +          let! ranty = Choice.List.fold (fun acc ty -> mk_fun_ty ty acc) ranty0 midtys
  +          if length domtys <= 1 then 
  +              return! ASSUME tm
             else 
  -              let dty = end_itlist (fun ty1 ty2 -> Choice.get <| mk_type("prod", [ty1; ty2])) domtys
  -              let f' = 
  -                  Choice.get 
  -                  <| variant (frees tm) (mk_var(fst(Choice.get <| dest_var f), Choice.get <| mk_fun_ty dty ranty))
  +              let! dty = Choice.List.reduceBack (fun ty1 ty2 -> mk_type("prod", [ty1; ty2])) domtys
  +              let! (tm1, _) = dest_var f
  +              let! tm2 = mk_fun_ty dty ranty
  +              let! f' = variant (frees tm) (mk_var(tm1, tm2))
                 let gvs = map genvar domtys
  -              let f'' = list_mk_abs(gvs, Choice.get <| mk_comb(f', end_itlist (curry(Choice.get << mk_pair)) gvs))
  -              let def' = Choice.get <| subst [f'', f] def
  -              let th1 = EXISTS (tm, f'') (ASSUME def')
  +              let! tm3 = mk_comb(f', end_itlist (curry(Choice.get << mk_pair)) gvs)
  +              let f'' = list_mk_abs(gvs, tm3)
  +              let! def' = subst [f'', f] def
  +              let! th1 = EXISTS (tm, f'') (ASSUME def')
                 let bth = BETAS_CONV(list_mk_comb(f'', gvs))
  -              let th2 = GEN_REWRITE_CONV TOP_DEPTH_CONV [bth] (hd(hyp <| Choice.get th1))
  -              SIMPLE_CHOOSE f' (PROVE_HYP (UNDISCH(snd(EQ_IMP_RULE th2))) th1)
  +              let th2 = GEN_REWRITE_CONV TOP_DEPTH_CONV [bth] (hd(hyp th1))
  +              return! SIMPLE_CHOOSE f' (PROVE_HYP (UNDISCH(snd(EQ_IMP_RULE th2))) (Choice.result th1))
  +         }
  +
         let pinstantiate_casewise_recursion def = 
  -          try 
  -              PART_MATCH Choice.result EXISTS_REFL def
  -          with
  -          | Failure _ -> 
  -              let f, bod = Choice.get <| dest_exists def
  +          PART_MATCH Choice.result EXISTS_REFL def
  +          |> Choice.bindError (function
  +              | Failure _ -> 
  +                choice {
  +                  let! f, bod = dest_exists def
  +                  let cjs = conjuncts bod
  +                  let eqs = map (snd << strip_forall) cjs
  +                  let! eqs' = Choice.List.map dest_eq eqs
  +                  let lefts, rights = unzip eqs'
  +                  let arglists = map (snd << strip_comb) lefts
  +                  let parms0 = freesl(unions arglists)
  +                  let parms = 
  +                      if parms0 <> [] then parms0
  +                      else [genvar aty]
  +                  let parm = end_itlist (curry(Choice.get << mk_pair)) parms
  +
  +                  let! ss = Choice.List.map (fun a -> 
  +                                choice {
  +                                    let tm1 = end_itlist (curry(Choice.get << mk_pair)) a
  +                                    return! mk_gabs(parm, tm1)
  +                                }) arglists
  +
  +                  let! ts = Choice.List.map (fun a -> 
  +                                choice {
  +                                    let! tm1 = mk_gabs(parm, a)
  +                                    return! mk_abs(f, tm1)
  +                                }) rights
  +
  +                  let! clauses = mk_flist(map2 (curry(Choice.get << mk_pair)) ss ts)
  +                  let pth = ISPEC clauses RECURSION_SUPERADMISSIBLE
  +                  let FIDDLE_CONV = 
  +                      (LAND_CONV << LAND_CONV << BINDER_CONV << RAND_CONV << LAND_CONV << GABS_CONV << RATOR_CONV << LAND_CONV 
  +                       << ABS_CONV)
  +                  let! th0 = UNDISCH(CONV_RULE (FIDDLE_CONV(LAMBDA_PAIR_CONV parms)) pth)
  +                  let th1 = EQ_MP (GEN_ALPHA_CONV f (concl th0)) (Choice.result th0)
  +                  let rewr_forall_th = REWR_CONV(FORALL_PAIR_CONV parm parms)
  +                  let! th2 = CONV_RULE (BINDER_CONV(LAND_CONV(GABS_CONV rewr_forall_th)
  +                                                   |> THENC <| EXPAND_PAIRED_ALL_CONV)) th1
  +                  let! f2, bod2 = dest_exists(concl th2)
  +                  let ths3 = 
  +                      map (CONV_RULE(COMB2_CONV (funpow 2 RAND_CONV GEN_BETA_CONV) (RATOR_CONV BETA_CONV
  +                                                                                    |> THENC <| GEN_BETA_CONV)) << SPEC_ALL) 
  +                          (CONJUNCTS(ASSUME bod2))
  +
  +                  let ths4 = 
  +                      map2 (fun th t -> 
  +                          let avs, tbod = strip_forall t
  +                          itlist GEN avs (PART_MATCH Choice.result th tbod)) ths3 cjs
  +                  let th5 = SIMPLE_EXISTS f (end_itlist CONJ ths4)
  +                  let! th6 = PROVE_HYP (Choice.result th2) (SIMPLE_CHOOSE f th5)
  +                  let th7 = (RAND_CONV
  +                                 (COMB2_CONV (RAND_CONV(LAND_CONV(GABS_CONV(BINDER_CONV(BINDER_CONV(rewr_forall_th)
  +                                                                                        |> THENC <| rewr_forall_th))))) 
  +                                      (LAND_CONV(funpow 2 GABS_CONV (BINDER_CONV(BINDER_CONV(rewr_forall_th)
  +                                                                                 |> THENC <| rewr_forall_th)))))
  +                             |> THENC <| ELIM_LISTOPS_CONV)(hd(hyp th6))
  +                  let! th8 = PROVE_HYP (UNDISCH(snd(EQ_IMP_RULE th7))) (Choice.result th6)
  +                  let wfasm, cdasm = Choice.get <| dest_conj(hd(hyp th8))
  +                  let th9 = PROVE_HYP (CONJ (ASSUME wfasm) (ASSUME cdasm)) (Choice.result th8)
  +                  let th10 = SIMPLIFY_WELLDEFINEDNESS_CONV cdasm
  +                  let th11 = PROVE_HYP (UNDISCH(snd(EQ_IMP_RULE th10))) th9
  +                  return! PROVE_HYP TRUTH th11
  +               }
  +              | e -> Choice.error e)
  +
  +      fun etm -> 
  +        choice {
  +          let! eth = tuple_function_existence etm
  +          let dtm = hd(hyp eth)
  +          let dth = pinstantiate_casewise_recursion dtm
  +          return! PROVE_HYP dth (Choice.result eth)
  +        }
  +      
  +      in
  +
  +(* ------------------------------------------------------------------------- *)
  +(* Justify existence assertion and try to simplify/remove side-conditions.   *)
  +(* ------------------------------------------------------------------------- *)
  +
  +  let pure_prove_recursive_function_exists = 
  +      let break_down_admissibility th1 = 
  +        choice {
  +          let! th1 = th1
  +          if hyp th1 = [] then 
  +              return th1
  +          else 
  +              let def = concl th1
  +              let! f, bod = dest_exists def
                 let cjs = conjuncts bod
                 let eqs = map (snd << strip_forall) cjs
  -              let lefts, rights = unzip(map (Choice.get << dest_eq) eqs)
  +              let! eqs' = Choice.List.map dest_eq eqs
  +              let lefts, rights = unzip eqs'
                 let arglists = map (snd << strip_comb) lefts
                 let parms0 = freesl(unions arglists)
                 let parms = 
                     if parms0 <> [] then parms0
                     else [genvar aty]
  -              let parm = end_itlist (curry(Choice.get << mk_pair)) parms
  -              let ss = map (fun a -> Choice.get <| mk_gabs(parm, end_itlist (curry(Choice.get << mk_pair)) a)) arglists
  -              let ts = map (fun a -> Choice.get <| mk_abs(f, Choice.get <| mk_gabs(parm, a))) rights
  -              let clauses = Choice.get <| mk_flist(map2 (curry(Choice.get << mk_pair)) ss ts)
  -              let pth = ISPEC clauses RECURSION_SUPERADMISSIBLE
  -              let FIDDLE_CONV = 
  -                  (LAND_CONV << LAND_CONV << BINDER_CONV << RAND_CONV << LAND_CONV << GABS_CONV << RATOR_CONV << LAND_CONV 
  -                   << ABS_CONV)
  -              let th0 = UNDISCH(CONV_RULE (FIDDLE_CONV(LAMBDA_PAIR_CONV parms)) pth)
  -              let th1 = EQ_MP (GEN_ALPHA_CONV f (concl <| Choice.get th0)) th0
  -              let rewr_forall_th = REWR_CONV(FORALL_PAIR_CONV parm parms)
  -              let th2 = CONV_RULE (BINDER_CONV(LAND_CONV(GABS_CONV rewr_forall_th)
  -                                               |> THENC <| EXPAND_PAIRED_ALL_CONV)) th1
  -              let f2, bod2 = Choice.get <| dest_exists(concl <| Choice.get th2)
  -              let ths3 = 
  -                  map (CONV_RULE(COMB2_CONV (funpow 2 RAND_CONV GEN_BETA_CONV) (RATOR_CONV BETA_CONV
  -                                                                                |> THENC <| GEN_BETA_CONV)) << SPEC_ALL) 
  -                      (CONJUNCTS(ASSUME bod2))
  -              let ths4 = 
  -                  map2 (fun th t -> 
  -                      let avs, tbod = strip_forall t
  -                      itlist GEN avs (PART_MATCH Choice.result th tbod)) ths3 cjs
  -              let th5 = SIMPLE_EXISTS f (end_itlist CONJ ths4)
  -              let th6 = PROVE_HYP th2 (SIMPLE_CHOOSE f th5)
  -              let th7 = (RAND_CONV
  -                             (COMB2_CONV (RAND_CONV(LAND_CONV(GABS_CONV(BINDER_CONV(BINDER_CONV(rewr_forall_th)
  -                                                                                    |> THENC <| rewr_forall_th))))) 
  -                                  (LAND_CONV(funpow 2 GABS_CONV (BINDER_CONV(BINDER_CONV(rewr_forall_th)
  -                                                                             |> THENC <| rewr_forall_th)))))
  -                         |> THENC <| ELIM_LISTOPS_CONV)(hd(hyp <| Choice.get th6))
  -              let th8 = PROVE_HYP (UNDISCH(snd(EQ_IMP_RULE th7))) th6
  -              let wfasm, cdasm = Choice.get <| dest_conj(hd(hyp <| Choice.get th8))
  -              let th9 = PROVE_HYP (CONJ (ASSUME wfasm) (ASSUME cdasm)) th8
  -              let th10 = SIMPLIFY_WELLDEFINEDNESS_CONV cdasm
  -              let th11 = PROVE_HYP (UNDISCH(snd(EQ_IMP_RULE th10))) th9
  -              PROVE_HYP TRUTH th11
  -      fun etm -> 
  -          let eth = tuple_function_existence etm
  -          let dtm = hd(hyp <| Choice.get eth)
  -          let dth = pinstantiate_casewise_recursion dtm
  -          PROVE_HYP dth eth
  -      
  -      in
  -
  -(* ------------------------------------------------------------------------- *)
  -(* Justify existence assertion and try to simplify/remove side-conditions.   *)
  -(* ------------------------------------------------------------------------- *)
  -
  -  let pure_prove_recursive_function_exists = 
  -      let break_down_admissibility th1 = 
  -          if hyp <| Choice.get th1 = [] then th1
  -          else 
  -              let def = concl <| Choice.get th1
  -              let f, bod = Choice.get <| dest_exists def
  -              let cjs = conjuncts bod
  -              let eqs = map (snd << strip_forall) cjs
  -              let lefts, rights = unzip(map (Choice.get << dest_eq) eqs)
  -              let arglists = map (snd << strip_comb) lefts
  -              let parms0 = freesl(unions arglists)
  -              let parms = 
  -                  if parms0 <> [] then parms0
  -                  else [genvar aty]
  -              let wfasm = Option.get <| find is_exists (hyp <| Choice.get th1)
  -              let ord, bod = Choice.get <| dest_exists wfasm
  +              let! wfasm = find is_exists (hyp th1) |> Option.toChoiceWithError "find"
  +              let! ord, bod = dest_exists wfasm
                 let SIMP_ADMISS_TAC = 
                     REWRITE_TAC [LET_DEF; LET_END_DEF]
                     |> THEN <| REPEAT ADMISS_TAC
  -                  |> THEN <| TRY(W(fun (asl, w) -> 
  -                                     let v = fst(Choice.get <| dest_forall w)
  -                                     X_GEN_TAC v
  -                                     |> THEN <| MAP_EVERY (fun v -> TRY(GEN_REWRITE_TAC I [FORALL_PAIR_THM])
  -                                                                    |> THEN <| X_GEN_TAC v) parms
  -                                     |> THEN <| CONV_TAC(TOP_DEPTH_CONV GEN_BETA_CONV)
  -                                     |> THEN <| MAP_EVERY (fun v -> SPEC_TAC(v, v)) (rev parms @ [v])))
  +                  |> THEN <| TRY(W(fun (asl, w) gl -> 
  +                                    choice {
  +                                    let! (v, _) = dest_forall w
  +                                    return!
  +                                        (X_GEN_TAC v
  +                                         |> THEN <| MAP_EVERY (fun v -> TRY(GEN_REWRITE_TAC I [FORALL_PAIR_THM])
  +                                                                        |> THEN <| X_GEN_TAC v) parms
  +                                         |> THEN <| CONV_TAC(TOP_DEPTH_CONV GEN_BETA_CONV)
  +                                         |> THEN <| MAP_EVERY (fun v -> SPEC_TAC(v, v)) (rev parms @ [v])) gl
  +                                    }))
                     |> THEN <| PURE_REWRITE_TAC [FORALL_SIMP]
                     |> THEN <| W(fun (asl, w) -> MAP_EVERY (fun t -> SPEC_TAC(t, t)) (subtract (frees w) [ord]))
                     |> THEN <| W(fun (asl, w) -> ACCEPT_TAC(ASSUME w))
  -              let th2 = prove(bod, SIMP_ADMISS_TAC)
  -              let th3 = SIMPLE_EXISTS ord th2
  -              let allasms = hyp <| Choice.get th3
  -              let wfasm = Choice.get <| lhand(concl <| Choice.get th2)
  +              let! th2 = prove(bod, SIMP_ADMISS_TAC)
  +              let! th3 = SIMPLE_EXISTS ord (Choice.result th2)
  +              let allasms = hyp th3
  +              let! wfasm = lhand(concl th2)
                 let th4 = ASSUME(list_mk_conj(wfasm :: subtract allasms [wfasm]))
  -              let th5 = SIMPLE_CHOOSE ord (itlist PROVE_HYP (CONJUNCTS th4) th3)
  -              PROVE_HYP th5 th1
  +              let th5 = SIMPLE_CHOOSE ord (itlist PROVE_HYP (CONJUNCTS th4) (Choice.result th3))
  +              return! PROVE_HYP th5 (Choice.result th1)
  +          }
         fun dtm -> 
  -          let th = break_down_admissibility(instantiate_casewise_recursion dtm)
  -          if concl <| Choice.get th = dtm then th
  -          else failwith "prove_general_recursive_function_exists: sanity"
  +        choice {
  +          let! th = break_down_admissibility(instantiate_casewise_recursion dtm)
  +          if concl th = dtm then 
  +              return th
  +          else 
  +              return! Choice.failwith "prove_general_recursive_function_exists: sanity"
  +        }
         
       in
   
  
positive.code:                          |> THEN <| REWRITE_TAC [MEASURE; MEASURE_LE]
                           |> THEN <| REWRITE_TAC [FORALL_PAIR_THM]
                           |> THEN <| GUESS_MEASURE_THEN tac))(asl, w)
        let PRE_GUESS_TAC = 
            CONV_TAC(BINDER_CONV(DEPTH_BINOP_CONV (parse_term @"(/\)") (TRY_CONV SIMPLIFY_WELLDEFINEDNESS_CONV
                                                                        |> THENC <| TRY_CONV FORALL_UNWIND_CONV)))
        let GUESS_ORDERING_TAC = 
            let false_tm = (parse_term @"\x:A y:A. F")
            W(fun (asl, w) -> 
                let ty = fst(Choice.get <| dest_fun_ty(Choice.get <| type_of(fst(Choice.get <| dest_exists w))))
                EXISTS_TAC(Choice.get <| inst [ty, aty] false_tm)
                |> THEN <| REWRITE_TAC [WF_FALSE]
                |> THEN <| NO_TAC)
            |> ORELSE <| GUESS_WF_THEN(REWRITE_TAC [FORALL_PAIR_THM]
                                       |> THEN <| ARITH_TAC)
        fun etm -> 
        let th = pure_prove_recursive_function_exists etm
        try 
            let wtm = Option.get <| find is_exists (hyp <| Choice.get th)
            let wth = prove(wtm, PRE_GUESS_TAC
                                 |> THEN <| GUESS_ORDERING_TAC)
            PROVE_HYP wth th
        with
        | Failure _ -> th
    
    in
  
  
negative.code:                 REPEAT STRIP_TAC
                  |> THEN <| EXISTS_TAC(parse_term @"\(x1:A,y1:B) (x2:A,y2:B). r x1 x2 \/ (x1 = x2) /\ s y1 y2")
                  |> THEN <| ASM_SIMP_TAC [WF_LEX])
  
        let pth_lexright = 
            prove((parse_term @"(?r. WF(r) /\
                ?s. WF(s) /\
  