proposition: Lemma fam_of_opp_sr g: allf g sgraph -> fam_of_substrates g = fam_of_substrates (fam_of_opp g).
proof: Proof. rewrite /fam_of_opp /fam_of_substrates; aw => h. apply: Lg_exten => i idg; aw; move: (h i idg) => sg. by rewrite LgV// /substrate (igraph_range sg) (igraph_domain sg) setU2_C. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)