anchor.diff:      (* ----------------------------------------------------------------------- *)
   
       let prove_model_inhabitation rth = 
  -        let srules = map SPEC_ALL (CONJUNCTS rth)
  -        let imps, bases = partition (is_imp << concl << Choice.get) srules
  -        let concs = map (concl << Choice.get) bases @ map (Choice.get << rand << concl << Choice.get) imps
  -        let preds = setify(map (repeat (Choice.toOption << rator)) concs)
  -        let rec exhaust_inhabitations ths sofar = 
  -            let dunnit = setify(map (fst << strip_comb << concl << Choice.get) sofar)
  -            let useful = 
  -                filter 
  -                    (fun th -> not(mem (fst(strip_comb(Choice.get <| rand(concl <| Choice.get th)))) dunnit)) 
  -                    ths
  -            if useful = []
  -            then sofar
  -            else 
  -                let follow_horn thm = 
  -                    let preds = 
  -                        map (fst << strip_comb) (conjuncts(Choice.get <| lhand(concl <| Choice.get thm)))
  -                    let asms = 
  -                        map 
  -                            (fun p -> 
  -                                Option.get <| find (fun th -> fst(strip_comb(concl <| Choice.get th)) = p) 
  -                                    sofar) preds
  -                    MATCH_MP thm (end_itlist CONJ asms)
  -                let newth = 
  -                    tryfind (Some << follow_horn) useful
  -                    |> Option.getOrFailWith "tryfind"
  -                exhaust_inhabitations ths (newth :: sofar)
  -        let ithms = exhaust_inhabitations imps bases
  -        let exths = 
  -            map (fun p -> Option.get <| find (fun th -> fst(strip_comb(concl <| Choice.get th)) = p) ithms) 
  -                preds
  -        exths
  +        choice {
  +            let srules = map SPEC_ALL (CONJUNCTS rth)
  +            let imps, bases = partition (is_imp << concl << Choice.get) srules
  +            let concs = map (concl << Choice.get) bases @ map (Choice.get << rand << concl << Choice.get) imps
  +            let preds = setify(map (repeat(Choice.toOption << rator)) concs)
  +        
  +            let rec exhaust_inhabitations ths sofar = 
  +                let dunnit = setify(map (fst << strip_comb << concl << Choice.get) sofar)
  +                let useful = filter (fun th -> not(mem (fst(strip_comb(Choice.get <| rand(concl <| Choice.get th)))) dunnit)) ths
  +                if useful = [] then sofar
  +                else 
  +                    let follow_horn thm = 
  +                        let preds = map (fst << strip_comb) (conjuncts(Choice.get <| lhand(concl <| Choice.get thm)))
  +                        let asms = 
  +                            map (fun p -> Option.get <| find (fun th -> fst(strip_comb(concl <| Choice.get th)) = p) sofar) preds
  +                        MATCH_MP thm (end_itlist CONJ asms)
  +                    let newth = tryfind (Choice.toOption << Choice.map Choice.result << follow_horn) useful |> Option.getOrFailWith "tryfind"
  +                    exhaust_inhabitations ths (newth :: sofar)
  +        
  +            let ithms = exhaust_inhabitations imps bases
  +            let exths = map (fun p -> Option.get <| find (fun th -> fst(strip_comb(concl <| Choice.get th)) = p) ithms) preds
  +        
  +            return exths
  +        }
  +
       (* ----------------------------------------------------------------------- *)
       (* Makes a type definition for one of the defined subsets.                 *)
       (* ----------------------------------------------------------------------- *)
  
positive.code: 
  /// Internal theorem list of distinctness theorems.
  let distinctness_store = ref ["bool", TAUT(parse_term @"(T <=> F) <=> F")]
  /// Internal theorem list of injectivity theorems.
  let injectivity_store = ref []
  
  
negative.code:         (* ----------------------------------------------------------------------- *)
          (* 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 = map (define_inductive_type defs) neths
          let preds = map (repeat (Choice.toOption << rator) << concl <<Choice.get) neths
          let mkdests = 
  