proposition: Lemma worders_quo_prop E x y a b: inc x (worders_quo E) -> inc y (worders_quo E) -> inc a x -> inc b y -> a \Is b -> x = y.
proof: Proof. move: (worders_eq_equivalence E) => ee xq yq ax bx isab. rewrite(worder_in_class_pr xq ax) (worder_in_class_pr yq bx). move:(worders_quo_isr xq ax) (worders_quo_isr yq bx) => asr bsr. by apply:(class_eq1 ee); apply/graph_on_P1. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)