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:         choice {
              let closed = list_mk_conj clauses
              let clauses = conjuncts closed
              let vargs, bodies = unzip(map strip_forall clauses)
              let ants, concs = unzip(map (Choice.get << dest_imp) bodies)
              let rels = map (repeat (Choice.toOption << rator)) concs
              let avoids = Choice.get <| variables closed
              let rels' = Choice.get <| variants avoids rels
              let crels = zip rels' rels
              let prime_fn = Choice.get << subst crels
              let closed' = prime_fn closed
              let mk_def arg con = 
                  Choice.get <| mk_eq
                      (repeat (Choice.toOption << rator) con, 
                       list_mk_abs
                           (arg, list_mk_forall(rels', Choice.get <| mk_imp(closed', prime_fn con))))
              let deftms = map2 mk_def vargs concs
              let defthms = map2 HALF_BETA_EXPAND vargs (map ASSUME deftms)
              let mk_ind args th = 
                  let th1 = fst(EQ_IMP_RULE(SPEC_ALL th))
                  let ant = Choice.get <| lhand(concl <| Choice.get th1)
                  let th2 = SPECL rels' (UNDISCH th1)
                  GENL args (DISCH ant (UNDISCH th2))
              let indthms = map2 mk_ind vargs defthms
              let indthmr = end_itlist CONJ indthms
              let indthm = GENL rels' (DISCH closed' indthmr)
              let mconcs = 
                  map2 (fun a t -> list_mk_forall(a, Choice.get <| mk_imp(t, prime_fn t))) vargs 
                      ants
              let monotm = Choice.get <| mk_imp(concl <| Choice.get indthmr, list_mk_conj mconcs)
              let monothm = 
                  ASSUME(list_mk_forall(rels, list_mk_forall(rels', monotm)))
              let closthm = ASSUME closed'
              let monothms = 
                  CONJUNCTS(MP (SPEC_ALL monothm) (MP (SPECL rels' indthm) closthm))
              let closthms = CONJUNCTS closthm
              let prove_rule mth (cth, dth) = 
                  let avs, bod = strip_forall(concl <| Choice.get mth)
                  let th1 = IMP_TRANS (SPECL avs mth) (SPECL avs cth)
                  let th2 = GENL rels' (DISCH closed' (UNDISCH th1))
                  let th3 = EQ_MP (SYM(SPECL avs dth)) th2
                  GENL avs (DISCH (Choice.get <| lhand bod) th3)
              let rulethms = map2 prove_rule monothms (zip closthms defthms)
              let rulethm = end_itlist CONJ rulethms
              let dtms = map2 (curry list_mk_abs) vargs ants
              let double_fn = Choice.get << subst(zip dtms rels)
              let mk_unbetas tm dtm = 
                  let avs, bod = strip_forall tm
                  let il, r = Choice.get <| dest_comb bod
                  let i, l = Choice.get <| dest_comb il
                  let bth = RIGHT_BETAS avs (REFL dtm)
                  let munb = AP_THM (AP_TERM i bth) r
                  let iunb = AP_TERM (Choice.get <| mk_comb(i, double_fn l)) bth
                  let junb = AP_TERM (Choice.get <| mk_comb(i, r)) bth
                  let quantify = itlist MK_FORALL avs
                  (quantify munb, (quantify iunb, quantify junb))
              let unths = map2 mk_unbetas clauses dtms
              let irthm = EQ_MP (SYM(end_itlist MK_CONJ (map fst unths))) rulethm
              let mrthm = MP (SPECL rels (SPECL dtms monothm)) irthm
              let imrth = 
                  EQ_MP (SYM(end_itlist MK_CONJ (map (fst << snd) unths))) mrthm
              let ifthm = MP (SPECL dtms indthm) imrth
              let fthm = EQ_MP (end_itlist MK_CONJ (map (snd << snd) unths)) ifthm
              let mk_case th1 th2 = 
                  let avs = fst(strip_forall(concl <| Choice.get th1))
                  GENL avs (IMP_ANTISYM_RULE (SPEC_ALL th1) (SPEC_ALL th2))
              let casethm = 
                  end_itlist CONJ (map2 mk_case (CONJUNCTS fthm) (CONJUNCTS rulethm))
              return! CONJ rulethm (CONJ indthm casethm)
          }
      fun tm -> 
          choice {
              let clauses = conjuncts tm
  
negative.code: /// Derive stronger induction theorem from inductive definition.
  let derive_strong_induction = 
      let dest_ibod tm = 
          choice {
              let avs, ibod = strip_forall tm
              let n = length avs
              let prator = funpow n (Choice.get << rator)
              let! ant, con = dest_imp ibod
              return n, (prator ant, prator con)
          }
  
      let rec prove_triv tm = 
          choice {
              if is_conj tm then
                  let! ltm = lhand tm
                  let! rtm = rand tm
                  return! CONJ (prove_triv ltm) (prove_triv rtm)
              else 
                  let avs, bod = strip_forall tm
                  let! a, c = dest_imp bod
                  let ths = CONJUNCTS(ASSUME a)
                  let! th = find (function | Success th -> aconv c (concl th)
                                           | Error _ -> false) ths
                            |> Option.toChoiceWithError "find"
                  return! GENL avs (DISCH a th)
          }
  
      let rec weaken_triv th = 
          choice {
              let! tm1 = Choice.map concl th
              if is_conj tm1 then 
                  return! CONJ (weaken_triv(CONJUNCT1 th)) (weaken_triv(CONJUNCT2 th))
              else 
                  let! avs, bod = Choice.map (strip_forall << concl) th
                  let th1 = SPECL avs th
                  let! (a, _) = Choice.bind (dest_imp << concl) th1
                  return! GENL avs (DISCH a (CONJUNCT2(UNDISCH th1)))
          }
  
  