proposition: Lemma sskeleton_subgraph_for (G : graph2) (V : {set G}) (E : {set edge G}) (con : consistent V E) (i o : sig [eta mem V]) : val i = input -> val o = output -> sgraph.subgraph (sskeleton (point (subgraph_for con) i o)) (sskeleton G).
proof: Proof. rewrite {2}/sskeleton/= => <- <-. exists val; first exact: val_inj. rewrite /hom_s. move => x y xy _. move: x y xy. apply sskelP. - move=> x y. by rewrite sg_sym. - move=> e sNt. apply/orP; left. apply/andP. split=> //. exact: adjacent_edge. - move=> /= iNo. by rewrite /edge_rel /= iNo !eqxx. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)