proposition: Lemma rts_extensionality1 r s x f g: order r -> inc x (substrate r) -> order s -> inc x (substrate s) -> segment r x = segment s x -> function f -> sub (segment r x) (source f) -> function g -> sub (segment s x) (source g) -> (forall a , inc a (segment r x) -> Vf f a = Vf g a) -> restriction1 f (segment r x) = restriction1 g (segment s x).
proof: Proof. move=> wor xsr wos xss srsx ff srf fg ssg sv. have rf: (restriction_to_segmentA r x f) by done. have rg: (restriction_to_segmentA s x g) by done. apply: function_exten =>//; try apply: rts_function1; try solve [rewrite /restriction1; aw;trivial]. rewrite /restriction1; aw; trivial. set_extens t. move/(Vf_image_P ff srf)=> [u us Wu]; apply /(Vf_image_P fg ssg). by rewrite - srsx; ex_tac; rewrite - sv. move/(Vf_image_P fg ssg)=> [u us Wu]; apply /(Vf_image_P ff srf). by rewrite - srsx in us; ex_tac; rewrite sv. move=> u;rewrite /restriction1; aw. move=> us. have p1: glt r u x by apply: (inc_segment us). have p2: glt s u x by rewrite srsx in us;apply: (inc_segment us); ue. rewrite rts_W1 // rts_W1 // sv //. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)