anchor.diff:          (* ----------------------------------------------------------------------- *)
           (* Basic function: returns induction and recursion separately. No parser.  *)
           (* ----------------------------------------------------------------------- *)
  -        let defs, rth, ith = justify_inductive_type_model def
  -        let neths = prove_model_inhabitation rth
  +        let defs, rth, ith = Choice.get <| justify_inductive_type_model def
  +        let neths = Choice.get <| prove_model_inhabitation rth
           let tybijpairs = map (define_inductive_type defs) neths
           let preds = map (repeat (Choice.toOption << rator) << concl <<Choice.get) neths
           let mkdests = 
  
positive.code:         let pasms = filter (C mem (map fst consindex) << Choice.get << lhand) (hyp <| Choice.get fxth5)
          let fxth6 = itlist DISCH pasms fxth5
          let fxth7, _ = 
              itlist SCRUB_EQUATION (itlist (union << hyp << Choice.get) conthms []) (fxth6, [])
          let fxth8 = UNDISCH_ALL fxth7
          fst(itlist SCRUB_EQUATION (subtract (hyp <| Choice.get fxth8) eqs) (fxth8, []))
  
      (* ----------------------------------------------------------------------- *)
      (* Create a function for recursion clause.                                 *)
  
negative.code:                 | Some (_, s2') ->
                      h1 :: (munion s1' s2')
                  | None -> h1 :: (munion s1' s2)
  
          fun def -> 
              choice {
                  let newtys, rights = unzip def
                  let tyargls = itlist ((@) << map snd) rights []
                  let alltys = itlist (munion << C subtract newtys) tyargls []
                  let! epstms = Choice.List.map (fun ty -> mk_select(mk_var("v", ty), t_tm)) alltys
  
                  let pty = 
                      // NOTE: review the order of arguments
                      Choice.List.reduceBack (fun ty1 ty2 -> mk_type("prod", [ty1; ty2])) alltys
                      |> Choice.fill bool_ty
  
                  let! recty = mk_type("recspace", [pty])
                  let! constr = mk_const("CONSTR", [pty, aty])
                  let! fcons = mk_const("FCONS", [recty, aty])
                  let! bot = mk_const("BOTTOM", [pty, aty])
                  let! bottail = mk_abs(n_tm, bot)
  
                  let mk_constructor n (cname, cargs) = 
                      choice {
                          let ttys = 
                              map (fun ty -> 
                                  if mem ty newtys then recty
                                  else ty) cargs
  
                          let! args = make_args "a" [] ttys
                          let rargs, iargs = partition (fun t -> Choice.get <| type_of t = recty) args
  
                          let rec mk_injector epstms alltys iargs = 
                              choice {
                                  if alltys = [] then 
                                      return []
                                  else 
                                      let ty = hd alltys
                                      return! 
                                          choice { 
                                              let! a, iargs' = 
                                                  remove (fun t -> Choice.get <| type_of t = ty) iargs
                                                  |> Option.toChoiceWithError "remove"
                                              let! tms = (mk_injector (tl epstms) (tl alltys) iargs')
                                              return a :: tms
                                          }
                                          |> Choice.bindError (fun _ -> 
                                                  choice {
                                                      let! tms = (mk_injector (tl epstms) (tl alltys) iargs)
                                                      return (hd epstms) :: tms
                                                  })
                              }
  
                          let! iarg = 
                              choice { 
                                  let! tms = mk_injector epstms alltys iargs
                                  return end_itlist (curry (Choice.get << mk_pair)) tms
                              }
                              |> Choice.bindError (fun _ -> Choice.result beps_tm)
  
                          let! rarg = Choice.List.fold (fun acc x -> mk_binop fcons x acc) bottail rargs
                          let! tms = Choice.List.map type_of args
                          let! conty = Choice.List.fold (fun acc ty -> mk_fun_ty ty acc) recty tms 
  
                          let condef = 
                              list_mk_comb(constr, [sucivate n; 
                                                    iarg; 
                                                    rarg])
  
                          return! mk_eq(mk_var(cname, conty), list_mk_abs(args, condef))
                      }
  
                  let rec mk_constructors n rights = 
                      choice {
                          if rights = [] then 
                              return []
                          else 
                              let! tms = mk_constructors (n + 1) (tl rights)
                              let! tm = mk_constructor n (hd rights)
                              return tm :: tms
                      }
  
                  let! condefs = mk_constructors 0 (itlist (@) rights [])
                  let conths = map ASSUME condefs
                  let! predty = mk_fun_ty recty bool_ty
  
                  let edefs = itlist (fun (x, l) acc -> map (fun t -> x, t) l @ acc) def []
                  let idefs = map2 (fun (r, (_, atys)) def -> (r, atys), def) edefs condefs
  
                  let mk_rule((r, a), condef) = 
                      choice {
                          let! left, right = dest_eq condef
                          let args, bod = strip_abs right
                          let lapp = list_mk_comb(left, args)
                      
                          let conds = 
                              itlist2 (fun arg argty sofar -> 
                                  if mem argty newtys then (Choice.get <| mk_comb(mk_var(Choice.get <| dest_vartype argty, predty), arg)) :: sofar
                                  else sofar) args a []
                      
                          let! tm1 = dest_vartype r
                          let! conc = mk_comb(mk_var(tm1, predty), lapp)
                      
                          let! rule = 
                              if conds = [] then Choice.result conc
                              else mk_imp(list_mk_conj conds, conc)
                      
                          return list_mk_forall(args, rule)
                      }
  
                  let! tms1 = Choice.List.map mk_rule idefs
                  let rules = list_mk_conj tms1
                  let th0 = derive_nonschematic_inductive_relations rules
                  let th1 = prove_monotonicity_hyps th0
                  let th2a, th2bc = CONJ_PAIR th1
                  let th2b = CONJUNCT1 th2bc
                  return conths, th2a, th2b
              }
  
      (* ----------------------------------------------------------------------- *)
      (* Shows that the predicates defined by the rules are all nonempty.        *)
  