proposition: Lemma transfinite_unique11 r p f f' z: order r -> inc z (substrate r) -> transfinite_def r p f -> transfinite_def r p f' -> (forall x : Set, inc x (segment r z) -> Vf f x = Vf f' x) -> restriction1 f (segment r z) = restriction1 f' (segment r z).
proof: Proof. move=> wo zsr [[ff _ ] sf Wf] [[ff' _] sf' Wf'] sW. have ss: sub (segment r z) (substrate r) by apply: sub_segment. apply: rts_extensionality1=> //; ue. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)