proposition: Lemma exercise3_1: [/\ has_no_graph (fun x y => inc x y), has_no_graph (fun x y => sub x y) & has_no_graph (fun x y => x = singleton y) ].
proof: Proof. split; apply: is_universal_pr; move=> x; [ exists (singleton x) | exists x | exists (singleton x) ] ; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)