-interpretation "Covers subsets" 'covers_subsets U V = (for_all _ U (covers _ V)).
-interpretation "Covers elem subset" 'covers_subsets U V = (covers _ V U).
+interpretation "Covers subsets" 'covers_subsets U V = (for_all ? U (covers ? V)).
+interpretation "Covers elem subset" 'covers_subsets U V = (covers ? V U).