proposition: Lemma Ex4_11_ex0_pure A R : inc emptyset R -> set_of_pure A R = emptyset.
proof: Proof. move => er; apply /set0_P => y; apply /set_of_pureP. move=>[_ h]; apply: h er; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)