- ∀O:ordered_uniform_space.∀l,r:O.
- ∀U:{[l,r]} squareO → Prop.∀u:O squareO → Prop.
- restriction_agreement ? l r U u →
- restriction_agreement ? l r (\inv U) (\inv u).
-intros 9; split; intro;
-[1: apply (unrestrict ????? (segment_square_of_ordered_set_square ??? 〈\snd b,\fst b〉 H2 H1) H H3);
-|2: apply (restrict ????? (segment_square_of_ordered_set_square ??? 〈\snd b,\fst b〉 H2 H1) H H3);]
+ ∀O:ordered_uniform_space.∀s:‡O.
+ ∀U:{[s]} squareO → Prop.∀u:O squareO → Prop.
+ restriction_agreement ? s U u →
+ restriction_agreement ? s (\inv U) (\inv u).
+intros 8; split; intro;
+[1: apply (unrestrict ???? (segment_square_of_ordered_set_square ?? 〈\snd b,\fst b〉 H2 H1) H H3);
+|2: apply (restrict ???? (segment_square_of_ordered_set_square ?? 〈\snd b,\fst b〉 H2 H1) H H3);]