theorem continuous_relation_eq':
∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
a = a' → ∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X).
theorem continuous_relation_eq':
∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
a = a' → ∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X).