proposition: Lemma not_collectivizing_notin: ~ (exists z, forall y, inc y z <-> not (inc y y)).
proof: Proof. case=> x hx; move: (hx x) => [p p']. pose H:= (fun h : inc x x => (p h h));exact (H (p' H)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)