proposition: Lemma CantorF r r' x y y': worder r' -> inc y (substrate r') -> inc y' (substrate r') -> (seg_order r x) \Is (seg_order r' y) -> (seg_order r x) \Is (seg_order r' y') -> y = y'.
proof: Proof. move => wor2 ysr ysr' is1 is2. exact:(CantorD wor2 ysr ysr' (orderIT (orderIS is1) is2)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)