proposition: Lemma dirim_set1_S f f': sgraph f -> sgraph f' -> ((forall x, sub (im_of_singleton f x) (im_of_singleton f' x)) <-> sub f f').
proof: Proof. move=> gr gr'; split=> s x t. move: (gr _ t) => eql; rewrite - eql;apply/dirim_set1_P. by apply: s; apply/dirim_set1_P; rewrite eql. by move/dirim_set1_P => jf; apply/dirim_set1_P; apply:s. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)