anchor.diff:  
   /// Produce distinctness theorem for an inductive type.
   let distinctness ty =
  -    assoc ty (!distinctness_store)
  -    |> Option.getOrFailWith "find"
  +    match assoc ty (!distinctness_store) with
  +    | Some x -> x
  +    | None -> Choice.failwith "find"
   
   /// Produce injectivity theorem for an inductive type.
   let injectivity ty =
  -    assoc ty (!injectivity_store)
  -    |> Option.getOrFailWith "find"
  +    match assoc ty (!injectivity_store) with
  +    | Some x -> x
  +    | None -> Choice.failwith "find"
   
   /// Produce cases theorem for an inductive type.
   let cases ty = 
  -    if ty = "num"
  -    then num_CASES
  -    else 
  -        let _, ith, _ =
  -            assoc ty (!inductive_type_store)
  -            |> Option.getOrFailWith "find"
  -        prove_cases_thm ith
  +    choice {
  +        if ty = "num" then 
  +            return! num_CASES
  +        else 
  +            let! _, ith, _ =
  +                assoc ty (!inductive_type_store)
  +                |> Option.toChoiceWithError "find"
  +
  +            return! prove_cases_thm ith
  +    }
   
   (* ------------------------------------------------------------------------- *)
   (* Convenient definitions for type isomorphism.                              *)
  
positive.code: 
      let TRIV_ANTE_RULE = 
          let TRIV_IMP_CONV tm = 
              let avs, bod = strip_forall tm
              let bth = 
                  if is_eq bod
                  then REFL(Choice.get <| rand bod)
                  else 
                      let ant, con = Choice.get <| dest_imp bod
                      let ith = SUBS_CONV (CONJUNCTS(ASSUME ant)) (Choice.get <| lhs con)
                      DISCH ant ith
              GENL avs bth
          fun th -> 
              let tm = concl <| Choice.get th
              if is_imp tm
              then 
                  let ant, con = Choice.get <| dest_imp(concl <| Choice.get th)
                  let cjs = conjuncts ant
                  let cths = map TRIV_IMP_CONV cjs
                  MP th (end_itlist CONJ cths)
              else th
  
      (* ----------------------------------------------------------------------- *)
      (* Lift type bijections to "arbitrary" (well, free rec or function) type.  *)
  
negative.code: 
  /// Extends internal store of distinctness and injectivity theorems for a new inductive type.
  let extend_rectype_net(tyname, (_, _, rth)) = 
      choice {
          let! ths1 = 
              choice { 
                  // NOTE: weird decomposition here
                  let! th = prove_constructors_distinct rth
                  return [Choice.result th]
              }
              |> Choice.bindError (fun _ -> Choice.result [])
  
          let! ths2 = 
              choice { 
                  let! th = prove_constructors_injective rth
                  return [Choice.result th]
              }
              |> Choice.bindError (fun _ -> Choice.result [])
  
          let! canon_thl = Choice.List.fold (fun acc x -> mk_rewrites false x acc) [] (ths1 @ ths2)
          distinctness_store := map (fun th -> tyname, th) ths1 @ (!distinctness_store)
          injectivity_store := map (fun th -> tyname, th) ths2 @ (!injectivity_store)
          let! tms = Choice.List.fold (fun acc x -> net_of_thm true x acc) (!basic_rectype_net) canon_thl
          basic_rectype_net := tms
      }
  
  do_list (ignore << extend_rectype_net) (!inductive_type_store);;
  
  (* ------------------------------------------------------------------------- *)
  (* Return distinctness and injectivity for a type by simple lookup.          *)
  