A brief report on trying to port the Iris hierarchy to HB about hierarchy-builder HOT 5 OPEN

HB: start module and section Sbi_of_Bi
HB: postulate type PROP
HB: postulate mixin_Bi_of_TYPE on PROP
HB: declare canonical instance PROP_is_a_bi
HB: declare record axioms_
HB: declare notation axioms
HB: declare notation Axioms
elpi: mk-phant-abbrev: T illtyped : 
Illegal application: 
The term "@Some" of type "∀ A : Type, A → option A"
cannot be applied to the terms
 "?e5" : "Type"
 "("is not canonically a", bi.type)" : "(string * Type)%type"
The 2nd term has type "(string * Type)%type" which should be coercible to
 "?e5".

(fun (_elpi_ctx_entry_0_ : ?e) (s : bi.type)
   (_ : @unify ?e1 ?e3 _elpi_ctx_entry_0_ (bi.sort s)
          (@Some ?e5
             (@pair ?e7 ?e9
                (String ... EmptyString))))))))))))))))))))
                bi.type))) (c : bi.axioms _elpi_ctx_entry_0_)
   (_ : @unify ?e11 ?e13 s (bi.Pack _elpi_ctx_entry_0_ c) (@None ?e15))
   (m : Bi_of_TYPE.axioms_ _elpi_ctx_entry_0_)
   (_ : @unify ?e17 ?e19 c (bi.Class _elpi_ctx_entry_0_ m) (@None ?e21))
   (sbi_later : forall _ : _elpi_ctx_entry_0_, _elpi_ctx_entry_0_)
   (sbi_internal_eq : forall (T : ofeT) (_ : ofe_car T) (_ : ofe_car T),
                      _elpi_ctx_entry_0_)
   (sbi_mixin_later_intro : forall P : _elpi_ctx_entry_0_,
                            @bi_entails (PROP_is_a_bi _elpi_ctx_entry_0_ m) P
                              (sbi_later P)) =>
 Axioms_ _elpi_ctx_entry_0_ m sbi_later sbi_internal_eq sbi_mixin_later_intro)