+Instance TyConToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }.
+Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }.
+
+Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
+Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".