proposition: Lemma sgraph_exten r r': sgraph r -> sgraph r' -> (forall u v, (related r u v <-> related r' u v)) -> r = r'.
proof: Proof. rewrite /related => gr gr' p. by set_extens t => tr; [move: (gr _ tr)=> pt | move: (gr' _ tr)=> pt]; rewrite - pt; apply /p; rewrite pt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)