anchor.diff:  let prove_constructors_injective = 
       let DEPAIR = GEN_REWRITE_RULE TOP_SWEEP_CONV [PAIR_EQ]
       let prove_distinctness ax pat = 
  -        let f, args = strip_comb pat
  -        let rt = end_itlist (curry (Choice.get << mk_pair)) args
  -        let ty = Choice.get <| mk_fun_ty (Choice.get <| type_of pat) (Choice.get <| type_of rt)
  -        let fn = genvar ty
  -        let dtm = Choice.get <| mk_eq(Choice.get <| mk_comb(fn, pat), rt)
  -        let eth = prove_recursive_functions_exist ax (list_mk_forall(args, dtm))
  -        let args' = Choice.get <| variants args args
  -        let atm = Choice.get <| mk_eq(pat, list_mk_comb(f, args'))
  -        let ath = ASSUME atm
  -        let bth = AP_TERM fn ath
  -        let cth1 = SPECL args (ASSUME(snd(Choice.get <| dest_exists(concl <| Choice.get eth))))
  -        let cth2 = INST (zip args' args) cth1
  -        let pth = TRANS (TRANS (SYM cth1) bth) cth2
  -        let qth = DEPAIR pth
  -        let qtm = concl <| Choice.get qth
  -        let rth = rev_itlist (C(curry MK_COMB)) (CONJUNCTS(ASSUME qtm)) (REFL f)
  -        let tth = IMP_ANTISYM_RULE (DISCH atm qth) (DISCH qtm rth)
  -        let uth = GENL args (GENL args' tth)
  -        PROVE_HYP eth (SIMPLE_CHOOSE fn uth)
  +        choice {
  +            let f, args = strip_comb pat
  +            let! rt = Choice.List.reduceBack (curry mk_pair) args
  +            let! ty = mk_fun_ty (Choice.get <| type_of pat) (Choice.get <| type_of rt)
  +            let fn = genvar ty
  +            let! dtm = mk_eq(Choice.get <| mk_comb(fn, pat), rt)
  +            let eth = prove_recursive_functions_exist ax (list_mk_forall(args, dtm))
  +            let! args' = variants args args
  +            let! atm = mk_eq(pat, list_mk_comb(f, args'))
  +            let ath = ASSUME atm
  +            let bth = AP_TERM fn ath
  +            let cth1 = SPECL args (ASSUME(snd(Choice.get <| dest_exists(concl <| Choice.get eth))))
  +            let cth2 = INST (zip args' args) cth1
  +            let pth = TRANS (TRANS (SYM cth1) bth) cth2
  +            let qth = DEPAIR pth
  +            let qtm = concl <| Choice.get qth
  +            let rth = rev_itlist (C(curry MK_COMB)) (CONJUNCTS(ASSUME qtm)) (REFL f)
  +            let tth = IMP_ANTISYM_RULE (DISCH atm qth) (DISCH qtm rth)
  +            let uth = GENL args (GENL args' tth)
  +            return! PROVE_HYP eth (SIMPLE_CHOOSE fn uth)
  +        }
  +
       fun ax -> 
  -        let cls = conjuncts(snd(strip_exists(snd(strip_forall(concl <| Choice.get ax)))))
  -        let pats = map (Choice.get << rand << Choice.get << lhand << snd << strip_forall) cls
  -        end_itlist CONJ (mapfilter (Some << prove_distinctness ax) pats);;
  +        choice {
  +            let cls = conjuncts(snd(strip_exists(snd(strip_forall(concl <| Choice.get ax)))))
  +            let pats = map (Choice.get << rand << Choice.get << lhand << snd << strip_forall) cls
  +            return! end_itlist CONJ (mapfilter (Some << prove_distinctness ax) pats)
  +        };;
   
   /// Proves that the constructors of an automatically-de ned concrete type yield distinct values.
  
positive.code:         else map (f(hd l)) (tl m) @ allopairs f (tl l) (tl m)
      let NEGATE = 
          GEN_ALL << CONV_RULE(REWR_CONV(TAUT(parse_term @"a ==> F <=> ~a")))
      let prove_distinct ax pat = 
          let nums = map (Choice.get << mk_small_numeral) (0 -- (length pat - 1))
          let fn = 
              genvar(Choice.get <| mk_type("fun", [Choice.get <| type_of(hd pat); num_ty]))
          let ls = map (curry (Choice.get << mk_comb) fn) pat
          let defs = 
              map2 (fun l r -> list_mk_forall(frees(Choice.get <| rand l), Choice.get <| mk_eq(l, r))) ls nums
          let eth = prove_recursive_functions_exist ax (list_mk_conj defs)
          let ev, bod = Choice.get <| dest_exists(concl <| Choice.get eth)
          let REWRITE = GEN_REWRITE_RULE ONCE_DEPTH_CONV (CONJUNCTS(ASSUME bod))
          let pat' = 
              map (fun t -> 
                      let f, args = 
                          if is_numeral t
                          then t, []
                          else strip_comb t
                      list_mk_comb(f, Choice.get <| variants args args)) pat
          let pairs = allopairs (curry (Choice.get << mk_eq)) pat pat'
          let nths = map (REWRITE << AP_TERM fn << ASSUME) pairs
          let fths = 
              map2 (fun t th -> NEGATE(DISCH t (CONV_RULE NUM_EQ_CONV th))) pairs 
                  nths
          CONJUNCTS(PROVE_HYP eth (SIMPLE_CHOOSE ev (end_itlist CONJ fths)))
      fun ax -> 
          let cls = conjuncts(snd(strip_exists(snd(strip_forall(concl <| Choice.get ax)))))
          let lefts = map (Choice.get << dest_comb << Choice.get << lhand << snd << strip_forall) cls
          let fns = itlist (insert << fst) lefts []
          let pats = map (fun f -> map snd (filter ((=) f << fst) lefts)) fns
          end_itlist CONJ (end_itlist (@) (mapfilter (Some << prove_distinct ax) pats));;
  
  (* ------------------------------------------------------------------------- *)
  (* Automatically prove the case analysis theorems.                           *)
  
negative.code:                     | _ -> failwith "mk_outls: Unhandled case."
              fun ty -> 
                  let x = mk_var("x", ty)
                  Choice.get <| Choice.List.map (curry mk_abs x) (mk_inls x ty)
          let mk_newfun fn outl = 
              let s, ty = Choice.get <| dest_var fn
              let dty = hd(snd(Choice.get <| dest_type ty))
  