GitLab

Here's what I've used:

(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *)
Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
  unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp,
         monPred_upclosed, bi_and, bi_or,
         bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
         bi_persistently, bi_affinely, bi_later;
  simpl.

(* Should be siProp.unseal. *)
Ltac siProp_unseal := unseal_prepare; siProp_primitive.unseal.

The second part is easy, but the first not (tho it was worse before the bi-sbi merge), and deserves to be abstracted.