anchor.diff:              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 = 
  -                        map (fun t -> Option.get <| find (fun th -> Choice.get <| lhs(concl <| Choice.get th) = t) ths) 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.get << rand) (Choice.get <| lhand(concl <| Choice.get th3))
  -                    let th4 = itlist (CONJ << REFL << fst) yes (ASSUME tm4)
  -                    let th5 = GENL args (GENL nvs (DISCH tm4 (MP th3 th4)))
  -                    let th6 = SPECL nvs (SPECL (map snd plis) (ASSUME(concl <| Choice.get th5)))
  -                    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 atm = list_mk_conj(map (Choice.get << mk_eq) (yes @ no))
  -                    let ths = CONJUNCTS(ASSUME atm)
  -                    let thl = 
  -                        map (fun t -> Option.get <| find (fun th -> Choice.get <| lhs(concl <| Choice.get th) = t) ths) 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.get << rand) (Choice.get <| lhand(concl <| Choice.get th3))
  -                    let th4 = itlist (CONJ << REFL << fst) yes (ASSUME tm4)
  -                    let th5 = GENL args (GENL nvs (DISCH tm4 (MP th3 th4)))
  -                    let th6 = SPECL nvs (SPECL (map snd plis) (ASSUME(concl <| Choice.get th5)))
  -                    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)
  +                    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.get << body << Choice.get << rand) (Choice.get <| rand(concl <| Choice.get eth))
  +            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))
           }
   
  
positive.code: 
      let make_definitions th = 
          choice {
              let defs = filter is_eq (hyp <| Choice.get th)
              let dths = map new_definition defs
              let insts = zip (map (Choice.get << lhs << concl << Choice.get) dths) (map (Choice.get << lhs) defs)
              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))
  
      let find_redefinition tm (rth, ith, cth as trip) = 
          if aconv tm (concl <| Choice.get rth)
          then trip
          else 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
  
      let prove_inductive_relations_exist tm = 
          let fvs, th1 = prove_inductive_properties tm
          let th2 = generalize_schematic_variables true fvs th1
          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 th2 = generalize_schematic_variables true fvs th1
              let th3 = make_definitions th2
              let avs = fst(strip_forall(concl <| Choice.get th3))
  
negative.code:         choice {
              let closed = list_mk_conj clauses
              let clauses = conjuncts closed
              let vargs, bodies = unzip (map strip_forall clauses)
              let! tms = Choice.List.map dest_imp bodies
              let ants, concs = unzip tms
              let rels = map (repeat (Choice.toOption << rator)) concs
              let! avoids = variables closed
              let! rels' = variants avoids rels
              let crels = zip rels' rels
              let prime_fn = subst crels
              let! closed' = prime_fn closed
              let mk_def arg con = 
                  choice {
                      let! tm = prime_fn con
                      let! tm' = mk_imp(closed', tm)
                      return! mk_eq(repeat (Choice.toOption << rator) con, 
                                    list_mk_abs (arg, list_mk_forall(rels', tm')))
                  }
  
              let! deftms = Choice.List.map2 mk_def vargs concs
              let defthms = map2 HALF_BETA_EXPAND vargs (map ASSUME deftms)
  
              let mk_ind args th = 
                  choice {
                      let th1 = fst(EQ_IMP_RULE(SPEC_ALL th))
                      let! ant = Choice.bind (lhand << concl) th1
                      let th2 = SPECL rels' (UNDISCH th1)
                      return! 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, Choice.get <| prime_fn t))) vargs ants
              let! tmr = Choice.map concl indthmr
              let! monotm = mk_imp(tmr, 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) = 
                  choice {
                      let! avs, bod = Choice.map (strip_forall << concl) 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
                      let! tm = lhand bod
                      return! GENL avs (DISCH tm 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 = subst (zip dtms rels)
  
              let mk_unbetas tm dtm = 
                  choice {
                      let avs, bod = strip_forall tm
                      let! il, r = dest_comb bod
                      let! i, l = dest_comb il
                      let bth = RIGHT_BETAS avs (REFL dtm)
                      let munb = AP_THM (AP_TERM i bth) r
                      let! tm1 = double_fn l
                      let! tm2 = mk_comb(i, tm1)
                      let iunb = AP_TERM tm2 bth
                      let! tm3 = mk_comb(i, r)
                      let junb = AP_TERM tm3 bth
                      let quantify = itlist MK_FORALL avs
                      return (quantify munb, (quantify iunb, quantify junb))
                  }
  
              let! unths = Choice.List.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 = 
                  choice {
                      let! avs = Choice.map (fst << strip_forall << concl) th1
                      return! 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
  