(tHOL4.min.bool,tHOL.bool);
(tHOL4.min.fun,tfun);
(tHOL4.num.num,tNat.nat);
(tHOL4.list.list,tList.list);
(tHOL4.pair.prod,tProduct_Type.prod);
(tHOL4.option.option,tOption.option);
(tHOL4.sum.sum,tSum_Type.sum);
(tHOL4.min.ind,tNat.ind);
  (tHOL4.patricia.ptree,tPredicate.seq);
  (tHOL4.llist.llist,tSet.set);
(tHOL4.integer.int,tInt.int);
  (tHOL4.extreal.extreal,tCode_Numeral.integer);
  (tHOL4.realax.real,tNum.num);
  (tHOL4.path.path,tQuickcheck_Narrowing.ffun);
(tHOL4.one.one,tProduct_Type.unit);
  (tHOL4.marker.label,tString.literal);
(tHOL4.bool.itself,titself);
  (tHOL4.ieee.ccode,tEnum.finite_4);
  (tHOL4.prelim.ordering,tEnum.finite_3);
  (tHOL4.string.char,tCode_Numeral.natural);
  (tHOL4.enumeral.bl,tQuickcheck_Exhaustive.three_valued);
  (tHOL4.canonical.canonical_sum,tQuickcheck_Exhaustive.unknown);
  (tHOL4.hreal.hreal,tExtraction.sumbool);
  (tHOL4.enumeral.bt,tLazy_Sequence.lazy_sequence);
(tHOL4.rat.rat,tEnum.finite_2);
(tHOL4.toto.cpn,tString.nibble);
(tHOL4.ieee.roundmode,tString.char);
(tHOL4.frac.frac,tCode_Evaluation.term);
(tHOL4.fcp.bit0,tQuickcheck_Narrowing.cfun);
(tHOL4.toto.num_dt,tSMT.pattern);
(tHOL4.lbtree.lbtree,tPredicate.pred)