Noting Rocq names when porting

Stream: iris-lean

[Markus de Medeiros]

In a recent PR, Michael brought up that it is helpful to be able to refer to the Rocq names for ported theorems. I think this is a great idea: not only will it help with porting, but it will make comparing Iris-Lean against Iris-Rocq for completeness a lot easier.

To link the two, Michael added in a deprecated alias:

theorem or_exists_bool [BI PROP] {P Q : PROP} :
    P ∨ Q ⊣⊢ «exists» (fun b : Bool => if b then P else Q) :=
  ⟨or_elim (exists_intro (Ψ:=λ b => if b then P else Q) true)
           (exists_intro (Ψ:=λ b => if b then P else Q) false),
   exists_elim (Bool.rec or_intro_r or_intro_l ·)⟩
@[deprecated or_exists_bool (since := "2026-01-29") ]
abbrev or_alt := @or_exists_bool -- name used by Iris Rocq

I suggest that we should make this a habit!