proposition: Lemma rts_W1 r x g a: restriction_to_segmentA r x g -> glt r a x -> Vf (restriction1 g (segment r x)) a = Vf g a.
proof: Proof. move=> [p1 p2 p3 p4] ax. by apply: restriction1_V =>//; apply/segmentP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)