proposition: Lemma CantorE r r' f f': worder r -> worder r' -> order_isomorphism f r r' -> order_isomorphism f' r r' -> f = f'.
proof: Proof. move => wor1 wor2 is1 is2. move: (is1) (is2) =>[_ _ [[[ff _] _]sf tf] _ ] [_ _ [[[ff' _] _] sf' tf'] _ ]. apply: function_exten=> //; (try ue); rewrite sf => x xsr. have fxr: inc (Vf f x) (substrate r') by Wtac. have gxr: inc (Vf f' x) (substrate r') by Wtac. move: (CantorA is1 xsr) (CantorA is2 xsr) => isi1 isi2. apply: (CantorD wor2 fxr gxr (orderIT (orderIS isi1) isi2)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)