characteristic predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type
A→Prop. *)
include "basics/types.ma".
include "basics/bool.ma".
characteristic predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type
A→Prop. *)
include "basics/types.ma".
include "basics/bool.ma".
definition empty_set ≝ λA:Type[0].λa:A.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
definition empty_set ≝ λA:Type[0].λa:A.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
notation "\emptyv" non associative with precedence 90 for @{'empty_set}.