equivI lemma for sigT
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?