proposition: Lemma related_in_quo E x a b: inc x (worders_quo E) -> inc a x -> inc b x -> related (worders_eq E) a b.
proof: Proof. move:(worders_eq_equivalence E) => ee. move/funI_P =>[z zr ->] /(class_P ee) r1 /(class_P ee) r2; equiv_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)