proposition: Lemma is_universal_pr r: is_universal r -> has_no_graph r.
proof: Proof. move=> u [X h]. case:(proj2 collectivizing_special). exists ((domain X) \cup (range X)) => y. move: (u y) => [x [] /h jg]; apply /setU2_P; [left | right];ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)