proposition: Lemma iso_one (G : graph2) : input == output :> G -> (forall x : G, x \in IO) -> (forall e : edge G, False) -> G ≃2 1.
proof: Proof. move => Dio A B. pose f (x : G) : g2_one := input. pose f' (x : g2_one) : G := input. pose g (e : edge G) : edge g2_one := match (B e) with end. pose g' (e : edge g2_one) : edge G := match e with end. unshelve Iso2 (@Iso _ _ _ _ (@Bij _ _ f f' _ _) (@Bij _ _ g g' _ _) xpred0 _)=>/=. - rewrite /f/f'/= => x. move: (A x). rewrite !inE -(eqP Dio) => /orP. by case => /eqP->. - by move => []. - by []. - by []. - by split. Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(bij set_tac digraph sgraph minor checkpoint) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(skeleton bounded equiv extraction_def)