Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
(* detects our crude Core-encoding of modal type introduction/elimination forms *)
Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
(* detects our crude Core-encoding of modal type introduction/elimination forms *)