λC:ordered_set.λU:C squareO → Prop.
λx:C squareO. U 〈\snd x,\fst x〉.
λC:ordered_set.λU:C squareO → Prop.
λx:C squareO. U 〈\snd x,\fst x〉.
-interpretation "relation invertion" 'invert a = (invert_os_relation _ a).
-interpretation "relation invertion" 'invert_symbol = (invert_os_relation _).
-interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x).
+interpretation "relation invertion" 'invert a = (invert_os_relation ? a).
+interpretation "relation invertion" 'invert_symbol = (invert_os_relation ?).
+interpretation "relation invertion" 'invert_appl a x = (invert_os_relation ? a x).
change in H1:(? ? ? %) with (\fst b);
change in a with (hos_carr (half_segment_ordered_set ? s));
change in b with (hos_carr (half_segment_ordered_set ? s));
change in H1:(? ? ? %) with (\fst b);
change in a with (hos_carr (half_segment_ordered_set ? s));
change in b with (hos_carr (half_segment_ordered_set ? s));
| right; change in H1:(? ? % ?) with (\fst b);
change in H1:(? ? ? %) with (\fst a);
change in a with (hos_carr (half_segment_ordered_set ? s));
change in b with (hos_carr (half_segment_ordered_set ? s));
| right; change in H1:(? ? % ?) with (\fst b);
change in H1:(? ? ? %) with (\fst a);
change in a with (hos_carr (half_segment_ordered_set ? s));
change in b with (hos_carr (half_segment_ordered_set ? s));