proposition: Lemma substrate_P r: sgraph r -> forall x, inc x (substrate r) <-> ((exists y, inc (J x y) r) \/ (exists y, inc (J y x) r)).
proof: Proof. move => gr x; split; last by case => [] [y yr]; substr_tac. by case /setU2_P => /funI_P [z zr ->]; [left | right]; ex_tac; rewrite gr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)