proposition: Lemma Ex4_11_ex3_pure A R: (forall x, inc x A -> inc (singleton x) R) -> (forall M, sub M A -> pure R M -> M = emptyset).
proof: Proof. move => asr m ma mb; case: (emptyset_dichot m) => em //. move: (rep_i em) => rm. by move: (set1_sub rm) => sm; case: (mb _ sm); apply: asr; apply: ma. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)