proposition: Lemma worders_quo_isr E x a: inc x (worders_quo E) -> inc a x -> inc a (worders E).
proof: Proof. move => xq ax; move: (inc_in_setQ_sr (worders_eq_equivalence E) ax xq). by rewrite worders_eq_sr. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)