GitLab

To use the new sigT construction, it helps to have an equivI lemma such as:

  Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
    x ≡ y ⊣⊢
    ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y : iProp Σ.
  Proof. by unseal. Qed.

@robbertkrebbers asks: should we have this just for iProp, or for any sbi?