anchor.diff:      let derive_recursion_theorem = 
           let CCONV = funpow 3 RATOR_CONV (REPEATC(GEN_REWRITE_CONV I [FCONS]))
           fun tybijpairs consindex conthms rath -> 
  -            let isocons = 
  -                map (create_recursion_iso_constructor consindex) conthms
  -            let ty = Choice.get <| type_of(hd isocons)
  -            let fcons = Choice.get <| mk_const("FCONS", [ty, aty])
  -            let fnil = Choice.get <| mk_const("FNIL", [ty, aty])
  -            let bigfun = itlist (fun x -> Choice.get << mk_binop fcons x) isocons fnil
  -            let eth = ISPEC bigfun CONSTR_REC
  -            let fn = Choice.get <| rator(Choice.get <| rand(hd(conjuncts(concl <| Choice.get rath))))
  -            let betm = 
  -                let v, bod = Choice.get <| dest_abs(Choice.get <| rand(concl <| Choice.get eth))
  -                Choice.get <| vsubst [fn, v] bod
  -            let LCONV = REWR_CONV(ASSUME betm)
  -            let fnths = 
  -                map (fun t -> RIGHT_BETAS [Choice.get <| bndvar(Choice.get <| rand t)] (ASSUME t)) 
  -                    (hyp <| Choice.get rath)
  -            let SIMPER = 
  -                PURE_REWRITE_RULE
  -                    (map SYM fnths 
  -                     @ map fst tybijpairs @ [FST; SND; FCONS; BETA_THM])
  -            let hackdown_rath th = 
  -                let ltm, rtm = Choice.get <| dest_eq(concl <| Choice.get th)
  -                let wargs = snd(strip_comb(Choice.get <| rand ltm))
  -                let th1 = TRANS th (LCONV rtm)
  -                let th2 = TRANS th1 (CCONV(Choice.get <| rand(concl <| Choice.get th1)))
  -                let th3 = 
  -                    TRANS th2 (funpow 2 RATOR_CONV BETA_CONV (Choice.get <| rand(concl <| Choice.get th2)))
  -                let th4 = TRANS th3 (RATOR_CONV BETA_CONV (Choice.get <| rand(concl <| Choice.get th3)))
  -                let th5 = TRANS th4 (BETA_CONV(Choice.get <| rand(concl <| Choice.get th4)))
  -                GENL wargs (SIMPER th5)
  -            let rthm = end_itlist CONJ (map hackdown_rath (CONJUNCTS rath))
  -            let seqs = 
  -                let unseqs = filter is_eq (hyp <| Choice.get rthm)
  -                let tys = 
  -                    map (hd << snd << Choice.get << dest_type << Choice.get << type_of << snd << snd) 
  -                        consindex
  -                map 
  -                    (fun ty -> 
  -                        Option.get <| find (fun t -> hd(snd(Choice.get <| dest_type(Choice.get <| type_of(Choice.get <| lhand t)))) = ty) unseqs) tys
  -            let rethm = itlist EXISTS_EQUATION seqs rthm
  -            let fethm = CHOOSE (fn, eth) rethm
  -            let pcons = 
  -                map (repeat (Choice.toOption << rator) << Choice.get << rand << repeat(Choice.toOption << Choice.map snd << dest_forall)) 
  -                    (conjuncts(concl <| Choice.get rthm))
  -            GENL pcons fethm
  +            choice {
  +                let! isocons = Choice.List.map (create_recursion_iso_constructor consindex) conthms
  +                let! ty = type_of(hd isocons)
  +                let! fcons = mk_const("FCONS", [ty, aty])
  +                let! fnil = mk_const("FNIL", [ty, aty])
  +                let bigfun = itlist (fun x -> Choice.get << mk_binop fcons x) isocons fnil
  +                let eth = ISPEC bigfun CONSTR_REC
  +                let fn = Choice.get <| rator(Choice.get <| rand(hd(conjuncts(concl <| Choice.get rath))))
  +                let betm = 
  +                    let v, bod = Choice.get <| dest_abs(Choice.get <| rand(concl <| Choice.get eth))
  +                    Choice.get <| vsubst [fn, v] bod
  +                let LCONV = REWR_CONV(ASSUME betm)
  +                let fnths = 
  +                    map (fun t -> RIGHT_BETAS [Choice.get <| bndvar(Choice.get <| rand t)] (ASSUME t)) 
  +                        (hyp <| Choice.get rath)
  +                let SIMPER = 
  +                    PURE_REWRITE_RULE
  +                        (map SYM fnths 
  +                         @ map fst tybijpairs @ [FST; SND; FCONS; BETA_THM])
  +                let hackdown_rath th = 
  +                    let ltm, rtm = Choice.get <| dest_eq(concl <| Choice.get th)
  +                    let wargs = snd(strip_comb(Choice.get <| rand ltm))
  +                    let th1 = TRANS th (LCONV rtm)
  +                    let th2 = TRANS th1 (CCONV(Choice.get <| rand(concl <| Choice.get th1)))
  +                    let th3 = 
  +                        TRANS th2 (funpow 2 RATOR_CONV BETA_CONV (Choice.get <| rand(concl <| Choice.get th2)))
  +                    let th4 = TRANS th3 (RATOR_CONV BETA_CONV (Choice.get <| rand(concl <| Choice.get th3)))
  +                    let th5 = TRANS th4 (BETA_CONV(Choice.get <| rand(concl <| Choice.get th4)))
  +                    GENL wargs (SIMPER th5)
  +                let rthm = end_itlist CONJ (map hackdown_rath (CONJUNCTS rath))
  +                let seqs = 
  +                    let unseqs = filter is_eq (hyp <| Choice.get rthm)
  +                    let tys = 
  +                        map (hd << snd << Choice.get << dest_type << Choice.get << type_of << snd << snd) 
  +                            consindex
  +                    map 
  +                        (fun ty -> 
  +                            Option.get <| find (fun t -> hd(snd(Choice.get <| dest_type(Choice.get <| type_of(Choice.get <| lhand t)))) = ty) unseqs) tys
  +                let rethm = itlist EXISTS_EQUATION seqs rthm
  +                let fethm = CHOOSE (fn, eth) rethm
  +                let pcons = 
  +                    map (repeat (Choice.toOption << rator) << Choice.get << rand << repeat(Choice.toOption << Choice.map snd << dest_forall)) 
  +                        (conjuncts(concl <| Choice.get rthm))
  +                return! GENL pcons fethm
  +            }
  +
       fun def -> 
  +
           (* ----------------------------------------------------------------------- *)
           (* Basic function: returns induction and recursion separately. No parser.  *)
           (* ----------------------------------------------------------------------- *)
  +
           let defs, rth, ith = Choice.get <| justify_inductive_type_model def
           let neths = Choice.get <| prove_model_inhabitation rth
           let tybijpairs = Choice.get <| Choice.List.map (define_inductive_type defs) neths
  
positive.code:         let PRERULE = GEN_REWRITE_RULE (funpow 3 RAND_CONV) (map SYM conthms)
          let IPRULE = SYM << GEN_REWRITE_RULE I (map snd tybijpairs)
          fun rthm tm -> 
              let avs, bimp = strip_forall tm
              if is_imp bimp
              then 
                  let ant, con = Choice.get <| dest_imp bimp
                  let ths = map (CONV_RULE BETA_CONV) (CONJUNCTS(ASSUME ant))
                  let tths, pths = unzip(map CONJ_PAIR ths)
                  let tth = MATCH_MP (SPEC_ALL rthm) (end_itlist CONJ tths)
                  let mths = map IPRULE (tth :: tths)
                  let conth1 = BETA_CONV con
                  let contm1 = Choice.get <| rand(concl <| Choice.get conth1)
                  let conth2 = 
                      TRANS conth1 
                          (AP_TERM (Choice.get <| rator contm1) 
                               (SUBS_CONV (tl mths) (Choice.get <| rand contm1)))
                  let conth3 = PRERULE conth2
                  let lctms = map (concl << Choice.get) pths
                  let asmin = Choice.get <| mk_imp(list_mk_conj lctms, Choice.get <| rand(Choice.get <| rand(concl <| Choice.get conth3)))
                  let argsin = map (Choice.get << rand) (conjuncts(Choice.get <| lhand asmin))
                  let argsgen = 
                      map (fun tm -> mk_var(fst(Choice.get <| dest_var(Choice.get <| rand tm)), Choice.get <| type_of tm)) 
                          argsin
                  let asmgen = Choice.get <| subst (zip argsgen argsin) asmin
                  let asmquant = 
                      list_mk_forall(snd(strip_comb(Choice.get <| rand(Choice.get <| rand asmgen))), asmgen)
                  let th1 = INST (zip argsin argsgen) (SPEC_ALL(ASSUME asmquant))
                  let th2 = MP th1 (end_itlist CONJ pths)
                  let th3 = EQ_MP (SYM conth3) (CONJ tth th2)
                  DISCH asmquant (GENL avs (DISCH ant th3))
              else 
                  let con = bimp
                  let conth2 = BETA_CONV con
                  let tth = PART_MATCH Choice.result rthm (Choice.get <| lhand(Choice.get <| rand(concl <| Choice.get conth2)))
                  let conth3 = PRERULE conth2
                  let asmgen = Choice.get <| rand(Choice.get <| rand(concl <| Choice.get conth3))
                  let asmquant = 
                      list_mk_forall(snd(strip_comb(Choice.get <| rand asmgen)), asmgen)
                  let th2 = SPEC_ALL(ASSUME asmquant)
                  let th3 = EQ_MP (SYM conth3) (CONJ tth th2)
                  DISCH asmquant (GENL avs th3)
  
      (* ----------------------------------------------------------------------- *)
      (* Finish off a consequence of the induction theorem.                      *)
  
negative.code:     (* ----------------------------------------------------------------------- *)
  
      let instantiate_induction_theorem consindex ith = 
          choice {
              let! ith = ith
              let avs, bod = strip_forall(concl ith)
              let! tm1 = rand bod
              let! corlist = 
                  Choice.List.map (Choice.map (repeat (Choice.toOption << rator) ||>> repeat (Choice.toOption << rator)) 
                                   << Choice.bind dest_imp << Choice.bind body << rand) (conjuncts tm1)
  
              let! consindex' = 
                  Choice.List.map (fun v -> 
                      choice {
                          let! w =
                              rev_assoc v corlist
                              |> Option.toChoiceWithError "find"
                          // TODO : Give this variable a better name.
                          let! x =
                              assoc w consindex
                              |> Option.toChoiceWithError "find"
                          return w, x
                      }) avs
  
              let! recty = (Choice.map hd << Choice.map snd << Choice.bind dest_type << type_of << fst << snd << hd) consindex
              let! newtys = Choice.List.map (Choice.map hd << Choice.map snd << Choice.bind dest_type << type_of << snd << snd) consindex'
  
              let ptypes = map (C (fun ty -> Choice.get << mk_fun_ty ty) bool_ty) newtys
  
              let! preds = make_args "P" [] ptypes
              let! args = make_args "x" [] (map (K recty) preds)
              let! lambs = 
                  Choice.List.map2 
                      (fun (r, (m, d)) (p, a) ->
                          choice {
                              let! tm0 = mk_comb(r, a)
                              let! tm1 = mk_comb(m, a)
                              let! tm2 = mk_comb(p, tm1)
                              let! tm3 = mk_conj(tm0, tm2)
                              return! mk_abs (a, tm3)
                          }) consindex' (zip preds args)
  
              return! SPECL lambs (Choice.result ith)
          }
  
      (* ----------------------------------------------------------------------- *)
      (* Reduce a single clause of the postulated induction theorem (old_ver) ba *)
  