proposition: Lemma lens_io_set (G : graph2) : lens G -> @edge_set _ _ G IO = edges input output :|: edges output input.
proof: Proof. move => /and3P [A B _]. apply/setP => e. apply/idP/idP. - rewrite !inE. (repeat let H := fresh in case: (boolP (_ == _)) => H) => //= _. + apply: contraTT A => _. apply/set0Pn; exists e. by rewrite inE (eqP H) (eqP H1) (@bag_id G). + apply: contraTT B => _. apply/set0Pn; exists e. by rewrite inE (eqP H0) (eqP H2) (@bag_id G). - by case/setUP ; apply: edge_in_set; rewrite !inE eqxx. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)