proposition: Lemma wordersP E r : inc r (worders E) <-> exists2 F, sub F E & worder_on r F.
proof: Proof. split. move/Zo_P => [/setP_P ha hb]; exists (substrate r) => // x xsr. by case /setXp_P: (ha _ (proj42 (proj1 hb) x xsr)). move => [F FE [wor sr]]; apply: Zo_i => //; apply/setP_P. move: (sub_graph_coarse_substrate (proj41 (proj1 wor))); rewrite sr => ss. exact: (sub_trans ss (setX_Sll FE)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)