- | reflexivity : ∀a.aεU → covers A U a
- | infinity : ∀a.∀i : I a. for_all A (C a i) (covers A U) → covers A U a.
+ | refl_ : ∀a.aεU → covers A U a
+ | infinity_ : ∀a.∀i : I a. for_all A (C a i) (covers A U) → covers A U a.
+
+notation "'refl'" non associative with precedence 90 for @{'refl}.
+interpretation "refl" 'refl = (refl_ _ _ _).
+
+notation "'infinity'" non associative with precedence 90 for @{'infinity}.
+interpretation "infinity" 'infinity = (infinity_ _ _ _).