interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b).
interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b).
interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b).
interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b).