(**** a subset of A is just an object of type A→Prop ****)
-definition empty_set ≝ λA:Type[0].λa:A.⊥.
+definition empty_set ≝ λA:Type[0].λa:A.False.
notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
interpretation "empty set" 'empty_set = (empty_set ?).