anchor.diff:      let ISO_EXPAND_CONV = PURE_ONCE_REWRITE_CONV [ISO]
   
       let rec lift_type_bijections iths cty = 
  -        let itys = 
  -            map (hd << snd << Choice.get << dest_type << Choice.get << type_of << Choice.get << lhand << concl <<Choice.get) iths
  -
  -        match assoc cty (zip itys iths) with
  -        | Some x -> x
  -        | None ->
  -            if not(exists (C occurs_in cty) itys)
  -            then INST_TYPE [cty, aty] ISO_REFL
  -            else 
  -                let tycon, isotys = Choice.get <| dest_type cty
  -                if tycon = "fun"
  -                then 
  -                    MATCH_MP ISO_FUN 
  -                        (end_itlist CONJ 
  -                             (map (lift_type_bijections iths) isotys))
  +        choice {
  +            let! itys = 
  +                Choice.List.map 
  +                    (Choice.map (hd << snd) << Choice.bind dest_type << Choice.bind type_of << Choice.bind lhand << Choice.map concl) iths
  +
  +            match assoc cty (zip itys iths) with
  +            | Some x -> 
  +                return! x
  +            | None -> 
  +                if not(exists (C occurs_in cty) itys) then 
  +                    return! INST_TYPE [cty, aty] ISO_REFL
                   else 
  -                    failwith
  -                        ("lift_type_bijections: Unexpected type operator \"" 
  -                         + tycon + "\"")
  +                    let! tycon, isotys = dest_type cty
  +                    if tycon = "fun" then
  +                        let ths = map (lift_type_bijections iths) isotys
  +                        return! MATCH_MP ISO_FUN (end_itlist CONJ ths)
  +                    else 
  +                        return! Choice.failwith("lift_type_bijections: Unexpected type operator \"" + tycon + "\"")
  +        }
   
       (* ----------------------------------------------------------------------- *)
       (* Prove isomorphism of nested types where former is the smaller.          *)
  
positive.code: 
  /// Extends internal store of distinctness and injectivity theorems for a new inductive type.
  let extend_rectype_net(tyname, (_, _, rth)) = 
      let ths1 = 
          try 
              [prove_constructors_distinct rth]
          with
          | Failure _ -> []
      let ths2 = 
          try 
              [prove_constructors_injective rth]
          with
          | Failure _ -> []
      let canon_thl = itlist (fun x y -> Choice.get <| mk_rewrites false x y) (ths1 @ ths2) []
      distinctness_store := map (fun th -> tyname, th) ths1 @ (!distinctness_store)
      injectivity_store := map (fun th -> tyname, th) ths2 @ (!injectivity_store)
      basic_rectype_net := itlist (fun x y -> Choice.get <| net_of_thm true x y) canon_thl (!basic_rectype_net)
  
  do_list extend_rectype_net (!inductive_type_store);;
  
  (* ------------------------------------------------------------------------- *)
  (* Return distinctness and injectivity for a type by simple lookup.          *)
  
negative.code:                  |> THEN <| DISCH_THEN SUBST1_TAC
                   |> THEN <| MATCH_MP_TAC SELECT_AX
                   |> THEN <| POP_ASSUM ACCEPT_TAC)
  
          let USE_PTH = MATCH_MP pth
  
          let rec DE_EXISTENTIALIZE_RULE th = 
              choice {
                  let! th = th
                  if not(is_exists(concl th)) then 
                      return [], th
                  else 
                      let! th1 = USE_PTH (Choice.result th)
                      let! tm1 = rand(concl th1)
                      let! v1 = rand tm1
                      let! ty1 = type_of v1
                      let gv = genvar ty1
                      let th2 = CONV_RULE BETA_CONV (UNDISCH(INST [gv, v1] (Choice.result th1)))
                      let! vs, th3 = DE_EXISTENTIALIZE_RULE th2
                      return gv :: vs, th3
              }
  
          DE_EXISTENTIALIZE_RULE
  
      let grab_type = Choice.bind type_of << Choice.bind rand << lhand << snd << strip_forall
  
      let clause_corresponds cl0 = 
          let v =
              choice {
                  let f0, ctm0 = Choice.get <| dest_comb(Choice.get <| lhs cl0)
                  let c0 = fst(Choice.get <| dest_const(fst(strip_comb ctm0)))
                  let dty0, rty0 = Choice.get <| dest_fun_ty(Choice.get <| type_of f0)
                  return (c0, dty0, rty0)
              }
          fun cl1 -> 
              choice {
                  let! (c0, dty0, rty0) = v
                  let! tm1 = lhs cl1
                  let! f1, ctm1 = dest_comb tm1
                  let! (c1, _) = dest_const(fst(strip_comb ctm1))
                  let! ty1 = type_of f1
                  let! dty1, rty1 = dest_fun_ty ty1
                  return c0 = c1 && dty0 = rty1 && rty0 = dty1
              }
  
      let prove_inductive_types_isomorphic n k (ith0, rth0) (ith1, rth1) = 
          choice {
          let! sth0 = SPEC_ALL rth0
          let! sth1 = SPEC_ALL rth1
          let! t_tm = Choice.map concl TRUTH
          let pevs0, pbod0 = strip_exists(concl sth0)
          let pevs1, pbod1 = strip_exists(concl sth1)
          let pcjs0, qcjs0 = chop_list k (conjuncts pbod0)
          let pcjs1, qcjs1 = chop_list k (snd(chop_list n (conjuncts pbod1)))
  
          let! pcjs1' = Choice.List.map grab_type pcjs1
          let! pcjs0' = Choice.List.map grab_type pcjs0
          let tyal0 = setify(zip pcjs1' pcjs0')
  
          let tyal1 = map (fun (a, b) -> (b, a)) tyal0
          let! tyins0 = 
              Choice.List.map (fun f -> 
                  choice {
                      let! tyf = type_of f
                      let! domty, ranty = dest_fun_ty tyf
                      let! ty1 = tysubst tyal0 domty
                      return ty1, ranty
                  }) pevs0
  
          let! tyins1 = 
              Choice.List.map (fun f -> 
                  choice {
                      let! tyf = type_of f
                      let! domty, ranty = dest_fun_ty tyf
                      let! ty1 = tysubst tyal1 domty
                      return ty1, ranty
                  }) pevs1
  
          let! tth0 = INST_TYPE tyins0 (Choice.result sth0)
          let! tth1 = INST_TYPE tyins1 (Choice.result sth1)
          let evs0, bod0 = strip_exists(concl tth0)
          let evs1, bod1 = strip_exists(concl tth1)
          let lcjs0, rcjs0 = chop_list k (map (snd << strip_forall) (conjuncts bod0))
          let lcjs1, rcjsx = 
              chop_list k (map (snd << strip_forall) (snd(chop_list n (conjuncts bod1))))
  
          let! rcjs1 = Choice.List.map (fun t -> Choice.List.find (clause_corresponds t) rcjsx) rcjs0
  
          let proc_clause tm0 tm1 = 
              choice {
              let! l0, r0 = dest_eq tm0
              let! l1, r1 = dest_eq tm1
              let vc0, wargs0 = strip_comb r0
              let! tm1 = rand l0
              let con0, vargs0 = strip_comb tm1
              let! gargs0 = Choice.List.map (Choice.map genvar << type_of) wargs0
              let! nestf0 =
                  Choice.List.map 
                      (fun a -> 
                          Choice.List.tryFind(fun t -> 
                              choice {
                                  let! tm = rand t
                                  return is_comb t && tm = a
                              }) wargs0
                          |> Choice.map Option.isSome) 
                      vargs0
  
              let! targs0 = 
                  Choice.List.map2 (fun a f -> 
                          if f then 
                              Choice.List.tryFind (fun t -> 
                                  choice {
                                      let! tm = rand t
                                      return is_comb t && tm = a
                                  }) wargs0
                              |> Choice.bind (Option.toChoiceWithError "find")
                          else Choice.result a) vargs0 nestf0
  
              let gvlist0 = zip wargs0 gargs0
              let! xargs =
                  targs0
                  |> Choice.List.map (fun v ->
                      assoc v gvlist0
                      |> Option.toChoiceWithError "find")
              
              let! tm1 = rand l1
              let inst0 = list_mk_abs (gargs0, list_mk_comb(fst(strip_comb tm1), xargs)), vc0
              let vc1, wargs1 = strip_comb r1
              let con1, vargs1 = strip_comb tm1
  
              let! gargs1 = Choice.List.map (Choice.map genvar << type_of) wargs1
              let! targs1 = 
                  Choice.List.map2 (fun a f -> 
                          if f then 
                              Choice.List.tryFind (fun t -> 
                                  choice {
                                      let! tm = rand t
                                      return is_comb t && tm = a
                                  }) wargs1
                              |> Choice.bind (Option.toChoiceWithError "find")
                          else Choice.result a) vargs1 nestf0
  
              let gvlist1 = zip wargs1 gargs1
              let! xargs =
                  targs1
                  |> Choice.List.map (fun v ->
                      assoc v gvlist1
                      |> Option.toChoiceWithError "find")
              
              let! tm2 = rand l0    
              let inst1 = list_mk_abs (gargs1, list_mk_comb(fst(strip_comb tm2), xargs)), vc1
              return inst0, inst1
              }
  
          let! insts = Choice.List.map2 proc_clause (lcjs0 @ rcjs0) (lcjs1 @ rcjs1)
          let insts0, insts1 = unzip insts
  
          let uth0 = BETA_RULE(INST insts0 (Choice.result tth0))
          let uth1 = BETA_RULE(INST insts1 (Choice.result tth1))
          let! efvs0, sth0 = DE_EXISTENTIALIZE_RULE uth0
          let! efvs1, sth1 = DE_EXISTENTIALIZE_RULE uth1
          let! efvs2 = 
              Choice.List.map (fun t1 -> 
                  Choice.List.tryFind(fun t2 -> 
                      choice {
                          let! ty1 = type_of t1
                          let! (_, tys2) = dest_type ty1
                          let! ty3 = type_of t2
                          let! (_, tys4) = dest_type ty3
                          return hd(tl tys2) = hd(tys4)
                      })  efvs1
                  |> Choice.bind (Option.toChoiceWithError "find")) efvs0
  
          let! isotms = Choice.List.map2 (fun ff gg -> list_mk_icomb "ISO" [ff; gg]) efvs0 efvs2
  
          let ctm = list_mk_conj isotms
          let! cth1 = ISO_EXPAND_CONV ctm
          let! ctm1 = rand(concl cth1)
          let cjs = conjuncts ctm1
          let eee = map (fun n -> n mod 2 = 0) (0 -- (length cjs - 1))
          let cjs1, cjs2 = partition fst (zip eee cjs)
          let! ctm2 = mk_conj(list_mk_conj(map snd cjs1), list_mk_conj(map snd cjs2))
          let DETRIV_RULE = TRIV_ANTE_RULE << REWRITE_RULE [Choice.result sth0; Choice.result sth1]
          let jth0 = 
              choice {
                  let! ith0 = ith0
  
                  let! itha = SPEC_ALL (Choice.result ith0)
                  let! tm1 = rand(concl itha)
                  let icjs = conjuncts tm1
                  let! tm2 = rand ctm2
                  let! cinsts = 
                      Choice.List.map (fun tm -> tryfind (fun vtm -> Choice.toOption <| term_match [] vtm tm) icjs
                                                 |> Option.toChoiceWithError "tryfind") (conjuncts tm2)
                  let tvs = subtract (fst(strip_forall(concl ith0))) (itlist (fun (_, x, _) -> union(map snd x)) cinsts [])
  
                  let! ctvs = 
                      Choice.List.map (fun p -> 
                          choice {
                              let! ty1 = type_of p
                              let! (_, tys2) = dest_type ty1
                              let x = mk_var("x", hd tys2)
                              let! tm2 = mk_abs(x, t_tm)
                              return tm2, p
                          }) tvs
  
                  return! DETRIV_RULE(INST ctvs (itlist INSTANTIATE cinsts (Choice.result itha)))
              }
  
          let jth1 = 
              choice {
                  let! ith1 = ith1
                  let! itha = SPEC_ALL (Choice.result ith1)
                  let! tm1 = rand(concl itha)
                  let icjs = conjuncts tm1
                  let! tm2 = lhand ctm2
                  let cinsts = 
                      map (fun tm -> tryfind (fun vtm -> Choice.toOption <| term_match [] vtm tm) icjs
                                     |> Option.getOrFailWith "tryfind") 
                          (conjuncts tm2)
  
                  let tvs = subtract (fst(strip_forall(concl ith1))) (itlist (fun (_, x, _) -> union(map snd x)) cinsts [])
  
                  let! ctvs = 
                      Choice.List.map (fun p -> 
                          choice {
                              let! ty1 = type_of p
                              let! (_, tys2) = dest_type ty1
                              let x = mk_var("x", hd tys2)
                              let! tm2 = mk_abs(x, t_tm)
                              return tm2, p
                          }) tvs
  
                  return! DETRIV_RULE(INST ctvs (itlist INSTANTIATE cinsts (Choice.result itha)))
              }
  
          let cths4 = map2 CONJ (CONJUNCTS jth0) (CONJUNCTS jth1)
          let cths5 = map (PURE_ONCE_REWRITE_RULE [GSYM ISO]) cths4
          let cth6 = end_itlist CONJ cths5
          return cth6, CONJ (Choice.result sth0) (Choice.result sth1)
          }
  
      (* ----------------------------------------------------------------------- *)
      (* Define nested type by doing a 1-level unwinding.                        *)
      (* ----------------------------------------------------------------------- *)
  
      let SCRUB_ASSUMPTION th = 
          choice {
              let! th = th
  
              let hyps = hyp th
              let! eqn = 
                  Choice.List.tryFind (fun t -> 
                      choice {
                          let! x = lhs t
                          return! Choice.List.forall (fun u -> 
                                      choice {
                                          let! tm = rand u
                                          return not(free_in x tm)
                                      }) hyps
                      }) hyps
                  |> Choice.bind (Option.toChoiceWithError "find")
  
              let! l, r = dest_eq eqn
              return! MP (INST [r, l] (DISCH eqn (Choice.result th))) (REFL r)
          }
  
      let define_type_basecase def = 
          let add_id s = fst(Choice.get <| dest_var(genvar bool_ty))
          let def' = map (I ||>> (map(add_id ||>> I))) def
          define_type_raw_002 def'
  
      let SIMPLE_BETA_RULE = GSYM << PURE_REWRITE_RULE [BETA_THM; FUN_EQ_THM]
      let ISO_USAGE_RULE = MATCH_MP ISO_USAGE
      let SIMPLE_ISO_EXPAND_RULE = CONV_RULE(REWR_CONV ISO)
  
      let REWRITE_FUN_EQ_RULE = 
          // NOTE: add these arguments to propagate errors
          fun tm gl ->
              choice {
                  let! ths = Choice.List.fold (fun acc x -> mk_rewrites false x acc) [] [FUN_EQ_THM]
                  let! net = Choice.List.fold (fun acc x -> net_of_thm false x acc) (basic_net()) ths
                  return! (CONV_RULE << GENERAL_REWRITE_CONV true TOP_DEPTH_CONV net) tm gl
              }
  
      let is_nested vs ty = 
          not(is_vartype ty) && not(intersect (tyvars ty) vs = [])
  
      let rec modify_type alist ty =
          match rev_assoc ty alist with
          | Some x -> x
          | None ->
              choice { 
                  let! tycon, tyargs = dest_type ty
                  return! mk_type(tycon, map (modify_type alist) tyargs)
              }
              |> Choice.fill ty
  
      let modify_item alist (s, l) = s, map (modify_type alist) l
      let modify_clause alist (l, lis) = l, map (modify_item alist) lis
  
      let recover_clause id tm = 
          choice {
              let con, args = strip_comb tm
              let! (s, _) = dest_const con
              let! tys = Choice.List.map type_of args
              return s + id, tys
          }
  
      let rec create_auxiliary_clauses nty = 
          choice {
              let! (id, _) = dest_var(genvar bool_ty)
              let! tycon, tyargs = dest_type nty
              let! k, ith, rth =
                  choice {
                      match assoc tycon !inductive_type_store with
                      | Some x -> 
                          return x
                      | None ->
                          return! Choice.failwith("Can't find definition for nested type: " + tycon)
                  }
              
              let! rth = rth
              let evs, bod = strip_exists(snd(strip_forall(concl rth)))
              let! cjs = Choice.List.map (lhand << snd << strip_forall) (conjuncts bod)
              let! rtys = Choice.List.map (Choice.map (hd << snd) << Choice.bind dest_type << type_of) evs
  
              let! tyins = tryfind (fun vty -> Choice.toOption <| type_match vty nty []) rtys 
                           |> Option.toChoiceWithError "tryfind"
  
              let! cjs' = Choice.List.map (Choice.bind (inst tyins) << rand) (fst(chop_list k cjs))
              let mtys = itlist (insert << Choice.get << type_of) cjs' []
  
              let! pcons = Choice.List.map (fun ty -> 
                                  Choice.List.filter (fun t -> 
                                      choice {
                                          let! ty1 = type_of t
                                          return ty1 = ty
                                      }) cjs') mtys
  
              let! tys = Choice.List.map (Choice.List.map(recover_clause id)) pcons
              let cls' = zip mtys tys
  
              let! tyal = Choice.List.map (fun ty -> 
                              choice {
                                  let! (s, _) = dest_type ty
                                  return mk_vartype(s + id), ty
                              }) mtys
  
              let cls'' = map (modify_type tyal ||>> map(modify_item tyal)) cls'
              return k, tyal, cls'', INST_TYPE tyins ith, INST_TYPE tyins (Choice.result rth)
          }
  
      let rec define_type_nested def = 
          choice {
          let n = length(itlist (@) (map (map fst << snd) def) [])
          let newtys = map fst def
          let utys = unions(itlist (union << map snd << snd) def [])
          let rectys = filter (is_nested newtys) utys
          if rectys = [] then 
              let th1, th2 = define_type_basecase def
              return n, th1, th2
          else 
              let nty = hd(sort (fun t1 t2 -> occurs_in t2 t1) rectys)
              let! k, tyal, ncls, ith, rth = create_auxiliary_clauses nty
              let cls = map (modify_clause tyal) def @ ncls
              let! _, ith1, rth1 = define_type_nested cls
              let! rth1' = rth1
              let! xnewtys = 
                  Choice.List.map (Choice.map (hd << snd) << Choice.bind dest_type << type_of) 
                      (fst(strip_exists(snd(strip_forall(concl rth1')))))
  
              let! xtyal = 
                  Choice.List.map (fun ty -> 
                      choice {
                          let! s = dest_vartype ty
                          let! ty1 = Choice.List.tryFind (fun t -> 
                                      choice {
                                          let! (s', _) = dest_type t
                                          return s' = s
                                      }) xnewtys
                                    |> Choice.bind (Option.toChoiceWithError "find")
  
                          return ty1, ty
                      }) (map fst cls)
                      
              let ith0 = INST_TYPE xtyal ith
              let rth0 = INST_TYPE xtyal rth
              let! isoth, rclauses = prove_inductive_types_isomorphic n k (ith0, rth0) (ith1, rth1)
              let! irth3 = CONJ ith1 rth1
  
              let! tm1 = variables(concl irth3)
              let vtylist = itlist (insert << Choice.get << type_of) tm1 []
              let isoths = CONJUNCTS isoth
              let! isotys = 
                  Choice.List.map (Choice.map (hd << snd) << Choice.bind dest_type 
                                   << Choice.bind type_of << Choice.bind lhand << Choice.map concl) isoths
  
              let ctylist = filter (fun ty -> exists (fun t -> occurs_in t ty) isotys) vtylist
              let atylist = itlist (union << striplist (Choice.toOption << dest_fun_ty)) ctylist []
              let isoths' = 
                  map (lift_type_bijections isoths) 
                      (filter (fun ty -> exists (fun t -> occurs_in t ty) isotys) atylist)
  
              let cisoths = map (BETA_RULE << lift_type_bijections isoths') ctylist
              let uisoths = map ISO_USAGE_RULE cisoths
  
              let! visoths = Choice.List.map (Choice.map (ASSUME << concl)) uisoths
              let irth4 = itlist PROVE_HYP uisoths (REWRITE_FUN_EQ_RULE visoths (Choice.result irth3))
              let irth5 = REWRITE_RULE (rclauses :: map SIMPLE_ISO_EXPAND_RULE isoths') irth4
              let! irth6 = repeat (Choice.toOption << Choice.map Choice.result << SCRUB_ASSUMPTION) irth5
  
              let! tm1 = rand(concl irth6)
              let! ncjs = 
                  Choice.List.filter (fun t -> 
                      choice {
                          let! tm2 = lhs(snd(strip_forall t))
                          let! tm3 = rand tm2 
                          return exists (fun v -> not(is_var v)) (snd(strip_comb tm3))
                      }) (conjuncts (snd (strip_exists (snd(strip_forall tm1)))))
  
              let mk_newcon tm = 
                  choice {
                      let vs, bod = strip_forall tm
                      let! tm1 = lhs bod
                      let! rdeb = rand tm1
                      let rdef = list_mk_abs(vs, rdeb)
                      let! (newname, _) = dest_var(genvar bool_ty)
                      let! ty1 = type_of rdef
                      let! def = mk_eq(mk_var(newname, ty1), rdef)
                      let dth = new_definition def
                      return! SIMPLE_BETA_RULE dth
                  }
  
              let dths = map mk_newcon ncjs
              let ith6, rth6 = CONJ_PAIR(PURE_REWRITE_RULE dths (Choice.result irth6))
              return n, ith6, rth6
          }
  
      fun def -> 
          choice {
              let newtys = map fst def
              let truecons = itlist (@) (map (map fst << snd) def) []
              let! (p, ith0, rth0) = define_type_nested def
              let! rth0 = rth0
              let avs, etm = strip_forall(concl rth0)
              let allcls = conjuncts(snd(strip_exists etm))
              let relcls = fst(chop_list (length truecons) allcls)
              let! gencons = 
                  Choice.List.map (Choice.map (repeat (Choice.toOption << rator)) << Choice.bind rand << lhand << snd << strip_forall) relcls
  
              let! cdefs = 
                  Choice.List.map2 (fun s r -> 
                      choice {
                          let! ty1 = type_of r
                          let! tm1 = mk_eq(mk_var(s, ty1), r)
                          return SYM(new_definition tm1)
                      }) truecons gencons
  
              let! tavs = make_args "f" [] (map (Choice.get << type_of) avs)
              let ith1 = SUBS cdefs ith0
              let rth1 = GENL tavs (SUBS cdefs (SPECL tavs (Choice.result rth0)))
              let retval = p, ith1, rth1
  
              let! newentries = Choice.List.map (fun s -> 
                                  choice {
                                      let! ty = dest_vartype s
                                      return ty , retval
                                  }) newtys
  
              inductive_type_store := newentries @ (!inductive_type_store)
              do_list (ignore << extend_rectype_net) newentries
              return ith1, rth1
           }
  
  (* ----------------------------------------------------------------------- *)
  (* The overall function, with rather crude string-based benignity.         *)
  