proposition: Lemma admissible_eqv_clot (l: pairs (union G1 G2)): (forall p, p \in l -> p.1 \in P /\ p.2 \in P) -> admissible (eqv_clot l).
proof: Proof. move => H x y. rewrite eqv_clotE. case/connectP => p. have relE u v : rel_of_pairs l u v -> ((u \in P) * (v \in P)) %type. { by move /H => /= [-> ->]. } elim: p x => /= [x _ -> //|z p IH x /andP [E pth_p] lst_p]; first by left. right. rewrite subUset !sub1set. case: (IH _ pth_p lst_p) => [Z|S]; subst. - rewrite -Z. case/orP : E => E; by rewrite !(relE _ _ E). - case/orP: E => E; rewrite (relE _ _ E) /=; by abstract (set_tac). Qed.
imports: Coq(RelationClasses Setoid) mathcomp(all_ssreflect) GraphTheory(edone set_tac finite_quotient preliminaries) GraphTheory(digraph sgraph treewidth minor equiv setoid_bigop) GraphTheory(structures mgraph pttdom ptt mgraph2 skeleton)