proposition: Lemma inclusion_morphism_b a b f : a <o b -> segmentp (ordinal_o b) (Imf f) -> order_morphism f (ordinal_o a) (ordinal_o b) -> (forall x, inc x a -> Vf f x = x).
proof: Proof. move => hlt s1 m1. move:(hlt) => [[oa ob sab] _]. move: (inclusion_morphism_a (proj1 hlt)) => [s2 m2]. rewrite (isomorphism_worder_unique (ordinal_o_wor oa)(ordinal_o_wor ob) s1 s2 m1 m2) => x xa; rewrite LfV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)