anchor.diff:  
       let make_definitions th = 
           choice {
  -            let defs = filter is_eq (hyp <| Choice.get th)
  +            let! tms = Choice.map hyp th
  +            let defs = filter is_eq tms
               let dths = map new_definition defs
  -            let insts = zip (map (Choice.get << lhs << concl << Choice.get) dths) (map (Choice.get << lhs) defs)
  +            let! tms1 = Choice.List.map (Choice.bind lhs << Choice.map concl) dths
  +            let! tms2 = Choice.List.map lhs defs
  +            let insts = zip tms1 tms2
               return! rev_itlist (C MP) dths (INST insts (itlist DISCH defs th))
           }
   
       let unschematize_clauses clauses = 
  -        let schem = 
  -            map (fun cls -> 
  -                    let avs, bod = strip_forall cls
  -                    pare_comb avs (try 
  -                                       snd(Choice.get <| dest_imp bod)
  -                                   with
  -                                   | Failure _ -> bod)) clauses
  -        let schems = setify schem
  -        if is_var(hd schem) then (clauses, [])
  -        elif not(length(setify(map (snd << strip_comb) schems)) = 1)
  -        then failwith "Schematic variables not used consistently"
  -        else 
  -            let avoids = Choice.get <| variables(list_mk_conj clauses)
  -            let hack_fn tm = mk_var(fst(Choice.get <| dest_var(repeat (Choice.toOption << rator) tm)), Choice.get <| type_of tm)
  -            let grels = Choice.get <| variants avoids (map hack_fn schems)
  -            let crels = zip grels schems
  -            let clauses' = map (Choice.get << subst crels) clauses
  -            clauses', snd(strip_comb(hd schems))
  +        choice {
  +            let! schem = 
  +                Choice.List.map (fun cls -> 
  +                        let avs, bod = strip_forall cls
  +                        pare_comb avs (match dest_imp bod with
  +                                       | Success(_, bod') -> bod'
  +                                       | Error _ -> bod)) clauses
  +            let schems = setify schem
  +            if is_var(hd schem) then 
  +                return (clauses, [])
  +            elif not(length(setify(map (snd << strip_comb) schems)) = 1) then 
  +                return! Choice.failwith "Schematic variables not used consistently"
  +            else 
  +                let! avoids = variables(list_mk_conj clauses)
  +                let hack_fn tm = 
  +                    choice {
  +                        let! (tm1, _) = dest_var(repeat (Choice.toOption << rator) tm)
  +                        let! ty = type_of tm
  +                        return mk_var(tm1, ty)
  +                    }
  +                let! tms = Choice.List.map hack_fn schems
  +                let! grels = variants avoids tms
  +                let crels = zip grels schems
  +                let! clauses' = Choice.List.map (subst crels) clauses
  +                return clauses', snd(strip_comb(hd schems))
  +        }
   
       let find_redefinition tm (rth, ith, cth as trip) = 
  -        if aconv tm (concl <| Choice.get rth)
  -        then trip
  -        else failwith "find_redefinition"
  +        choice {
  +            let! tm1 = Choice.map concl rth
  +            if aconv tm tm1 then 
  +                return trip
  +            else 
  +                return! Choice.failwith "find_redefinition"
  +        }
   
       let prove_inductive_properties tm = 
  -        let clauses = conjuncts tm
  -        let clauses', fvs = unschematize_clauses clauses
  -        let th = derive_nonschematic_inductive_relations(list_mk_conj clauses')
  -        fvs, prove_monotonicity_hyps th
  +        choice {
  +            let clauses = conjuncts tm
  +            let! clauses', fvs = unschematize_clauses clauses
  +            let th = derive_nonschematic_inductive_relations(list_mk_conj clauses')
  +            return fvs, prove_monotonicity_hyps th
  +        }
   
       let prove_inductive_relations_exist tm = 
  -        let fvs, th1 = prove_inductive_properties tm
  -        let th2 = generalize_schematic_variables true fvs th1
  -        derive_existence th2
  +        choice {
  +            let! fvs, th1 = prove_inductive_properties tm
  +            let th2 = generalize_schematic_variables true fvs th1
  +            return! derive_existence th2
  +        }
   
       let new_inductive_definition tm = 
  -        try 
  -            let th = tryfind (Some << find_redefinition tm) (!the_inductive_definitions)
  -                     |> Option.getOrFailWith "tryfind"
  -            warn true "Benign redefinition of inductive predicate"
  -            th
  -        with
  -        | Failure _ -> 
  -            let fvs, th1 = prove_inductive_properties tm
  +         
  +        let th = tryfind (Choice.toOption << find_redefinition tm) (!the_inductive_definitions)
  +                 |> Option.toChoiceWithError "tryfind"
  +        warn true "Benign redefinition of inductive predicate"
  +        match th with
  +        | Success th -> th
  +        | Error _ ->
  +            // NOTE: this part is unsafe
  +            let fvs, th1 = Choice.get <| prove_inductive_properties tm
               let th2 = generalize_schematic_variables true fvs th1
               let th3 = make_definitions th2
               let avs = fst(strip_forall(concl <| Choice.get th3))
  
positive.code:                             (gvs, 
                               Choice.get <| mk_conj(list_mk_comb(r, gvs), list_mk_comb(p, gvs)))) 
                      ns prrs
              let modify_rule rcl itm = 
                  let avs, bod = strip_forall itm
                  if is_imp bod
                  then 
                      let a, c = Choice.get <| dest_imp bod
                      let mgoal = Choice.get <| mk_imp(gimps, Choice.get <| mk_imp(Choice.get <| vsubst (zip gs ps) a, a))
                      let mth = ASSUME(list_mk_forall(gs @ ps @ avs, mgoal))
                      let ith_r = BETA_RULE(SPECL (prs @ rs @ avs) mth)
                      let jth_r = MP ith_r (prove_triv(Choice.get <| lhand(concl <| Choice.get ith_r)))
                      let t = Choice.get <| lhand(concl <| Choice.get jth_r)
                      let kth_r = UNDISCH jth_r
                      let ntm = list_mk_forall(avs, Choice.get <| mk_imp(t, c))
                      let lth_r = MP (SPECL avs rcl) kth_r
                      let lth_p = UNDISCH(SPECL avs (ASSUME ntm))
                      DISCH ntm (GENL avs (DISCH t (CONJ lth_r lth_p)))
                  else 
                      DISCH itm (GENL avs (CONJ (SPECL avs rcl) (SPECL avs (ASSUME itm))))
              let mimps = map2 modify_rule (CONJUNCTS sth) (conjuncts iant)
              let th1 = end_itlist (fun th th' -> MATCH_IMPS(CONJ th th')) mimps
              let th2 = BETA_RULE(SPECL prs jth)
              let th3 = IMP_TRANS th1 th2
              let nasm = Choice.get <| lhand(concl <| Choice.get th3)
              let th4 = GENL ps (DISCH nasm (weaken_triv(UNDISCH th3)))
              return! GENL svs (prove_monotonicity_hyps th4)
          }
  
negative.code:             let nvs = filter (not << C mem (map snd yes)) avs
              let eth = 
                  choice {
                      if is_imp bimp then 
                          let atm = itlist (curry (Choice.get << mk_conj) << Choice.get << mk_eq) (yes @ no) ant
                          let ths, tth = nsplit CONJ_PAIR plis (ASSUME atm)
                          let! thl = Choice.List.map (fun t -> 
                                          find (fun th -> match Choice.bind (lhs << concl) th with
                                                          | Success t' when t' = t -> true
                                                          | _ -> false) ths
                                          |> Option.toChoiceWithError "find") args
  
                          let th0 = MP (SPECL avs (ASSUME cls)) tth
                          let th1 = rev_itlist (C(curry MK_COMB)) thl (REFL rel)
                          let th2 = EQ_MP (SYM th1) th0
                          let th3 = INST yes (DISCH atm th2)
                          let! tm4 = funpow (length yes) (Choice.bind rand) (Choice.bind (lhand << concl) th3)
                          let th4 = itlist (CONJ << REFL << fst) yes (ASSUME tm4)
                          let th5 = GENL args (GENL nvs (DISCH tm4 (MP th3 th4)))
                          let! tm5 = Choice.map concl th5
                          let th6 = SPECL nvs (SPECL (map snd plis) (ASSUME tm5))
                          let th7 = itlist (CONJ << REFL << snd) no (ASSUME ant)
                          let th8 = GENL avs (DISCH ant (MP th6 th7))
                          return! IMP_ANTISYM_RULE (DISCH_ALL th5) (DISCH_ALL th8)
                      else
                          let! tms = Choice.List.map mk_eq (yes @ no)
                          let atm = list_mk_conj tms
                          let ths = CONJUNCTS(ASSUME atm)
                          let! thl = Choice.List.map (fun t -> 
                                          find (fun th -> match Choice.bind (lhs << concl) th with
                                                          | Success t' when t' = t -> true
                                                          | _ -> false) ths
                                          |> Option.toChoiceWithError "find") args
                          let th0 = SPECL avs (ASSUME cls)
                          let th1 = rev_itlist (C(curry MK_COMB)) thl (REFL rel)
                          let th2 = EQ_MP (SYM th1) th0
                          let th3 = INST yes (DISCH atm th2)
                          let! tm4 = funpow (length yes) (Choice.bind rand) (Choice.bind (lhand << concl) th3)
                          let th4 = itlist (CONJ << REFL << fst) yes (ASSUME tm4)
                          let th5 = GENL args (GENL nvs (DISCH tm4 (MP th3 th4)))
                          let! tm5 = Choice.map concl th5
                          let th6 = SPECL nvs (SPECL (map snd plis) (ASSUME tm5))
                          let th7 = end_itlist CONJ (map (REFL << snd) no)
                          let th8 = GENL avs (MP th6 th7)
                          return! IMP_ANTISYM_RULE (DISCH_ALL th5) (DISCH_ALL th8)
                  }
              let! ftm = funpow (length args) (Choice.bind (Choice.bind body << rand)) (Choice.bind (rand << concl) eth)
              return! TRANS eth (itlist MK_FORALL args (FORALL_IMPS_CONV ftm))
          }
  
  