proposition: Lemma iso_top (G : graph2) : input != output :> G -> (forall x : G, x \in IO) -> (forall e : edge G, False) -> G ≃2 top.
proof: Proof. move => Dio A B. pose f (x : G) : g2_top := if x == input then input else output. pose f' (x : g2_top) : G := if x == input then input else output. pose g (e : edge G) : edge g2_top := match (B e) with end. pose g' (e : edge g2_top) : edge G := match e with inl e |inr e => vfun e end. unshelve Iso2 (@Iso _ _ _ _ (@Bij _ _ f f' _ _) (@Bij _ _ g g' _ _) xpred0 _)=>/=. - rewrite /f/f'/= => x. case: (boolP (x == input)) => [/eqP <-|/=]//. move: (A x). case/setUP => /set1P => -> //. by rewrite eqxx. - rewrite /f/f'/= => x. case: (boolP (x == inl tt)) => [/eqP <-|/=]//. by rewrite eqxx. case: x => // [[]] _. by rewrite eq_sym (negbTE Dio). - by []. - by case=>[[]|[]]. - by split. - by rewrite /f eqxx. - by rewrite /f eq_sym (negbTE Dio). 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)