include "formal_topology/basic_pairs.ma".
include "formal_topology/o-basic_pairs.ma".
include "formal_topology/relations_to_o-algebra.ma".
-
+(*
definition o_basic_pair_of_basic_pair: basic_pair → Obasic_pair.
intro b;
constructor 1;
| change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);]
simplify; apply (†(Hgc‡#));
qed.
+*)