From cabbf857808d1e01d6c1315155ef28c4f28e383a Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Wed, 8 Jul 2026 16:58:36 +0200
Subject: [PATCH 01/12] Generalise `asEmpValid_2` for various `InOut` values

---
 Iris/Iris/ProofMode/Classes.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
index ac2ca161b..2d561e243 100644
--- a/Iris/Iris/ProofMode/Classes.lean
+++ b/Iris/Iris/ProofMode/Classes.lean
@@ -30,13 +30,13 @@ inductive AsEmpValid.Direction where
 class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) (_ : InOut) (PROP : semiOutParam $ Type _)
 (_ : InOut) (bi : semiOutParam $ BI PROP) (P : outParam $ PROP) where
   as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ)
-
 @[rocq_alias as_emp_valid_1]
 theorem asEmpValid_1 {PROP} [bi : BI PROP] {φ : Prop} (P : PROP) [AsEmpValid .into φ .in PROP .in bi P]
 : φ → ⊢ P := (AsEmpValid.as_emp_valid .in .in).1 rfl
 @[rocq_alias as_emp_valid_2]
-theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (φ : Prop) [AsEmpValid .from φ .out PROP .out bi P]
-: (⊢ P) → φ := (AsEmpValid.as_emp_valid .out .out).2 rfl
+theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (io : InOut)
+    (φ : Prop) (inst : AsEmpValid .from φ io PROP .out bi P) : (⊢ P) → φ :=
+  (AsEmpValid.as_emp_valid io .out).2 rfl
 
 /- Depending on the use case, type classes with the prefix `From` or `Into` are used. Type classes
 with the prefix `From` are used to generate one or more propositions *from* which the original

From c2aa27ad113513d1cca4193f6590eaf976ce57ef Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Wed, 8 Jul 2026 17:01:45 +0200
Subject: [PATCH 02/12] Implement `istart` with specific BI instance

---
 Iris/Iris/ProofMode/Classes.lean       |  2 +-
 Iris/Iris/ProofMode/ProofModeM.lean    | 27 +++++++++++++++++++++-----
 Iris/Iris/ProofMode/Tactics/Basic.lean | 11 ++++++++++-
 3 files changed, 33 insertions(+), 7 deletions(-)

diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
index 2d561e243..9e4167312 100644
--- a/Iris/Iris/ProofMode/Classes.lean
+++ b/Iris/Iris/ProofMode/Classes.lean
@@ -34,7 +34,7 @@ class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) (_ : InOut) (PROP : semi
 theorem asEmpValid_1 {PROP} [bi : BI PROP] {φ : Prop} (P : PROP) [AsEmpValid .into φ .in PROP .in bi P]
 : φ → ⊢ P := (AsEmpValid.as_emp_valid .in .in).1 rfl
 @[rocq_alias as_emp_valid_2]
-theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (io : InOut)
+theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} {io : InOut}
     (φ : Prop) (inst : AsEmpValid .from φ io PROP .out bi P) : (⊢ P) → φ :=
   (AsEmpValid.as_emp_valid io .out).2 rfl
 
diff --git a/Iris/Iris/ProofMode/ProofModeM.lean b/Iris/Iris/ProofMode/ProofModeM.lean
index f20e854f6..e56ec1d4b 100644
--- a/Iris/Iris/ProofMode/ProofModeM.lean
+++ b/Iris/Iris/ProofMode/ProofModeM.lean
@@ -109,28 +109,45 @@ def ProofModeM.synthInstanceQ (α : Q(Sort v)) : ProofModeM Q($α) := do
   return e
 
 /-- Initialize proof mode for a metavariable, converting it to an Iris goal. -/
-def startProofMode (mvar : MVarId) : MetaM (MVarId × IrisGoal) := mvar.withContext do
+def startProofMode (mvar : MVarId) (customProp : Option Expr := none) :
+    MetaM (MVarId × IrisGoal) := mvar.withContext do
   -- parse goal
   let goal ← instantiateMVars <| ← mvar.getType
 
   -- check if already in proof mode
   if let some irisGoal := parseIrisGoal? goal then
-    return (mvar, irisGoal)
+    match customProp with
+    | none =>
+      return (mvar, irisGoal)
+    | some customProp =>
+      let eq ← isDefEq irisGoal.prop customProp
+      if !eq then
+        throwError "istart: currently in the Iris Proof Mode with {irisGoal.prop} rather than {customProp}"
+      return (mvar, irisGoal)
 
   let some goal ← checkTypeQ goal q(Prop)
     | throwError "type mismatch\n{← mkHasTypeButIsExpectedMsg (← inferType goal) q(Prop)}"
   let u ← mkFreshLevelMVar
   let prop ← mkFreshExprMVarQ q(Type u)
+
+  if let some p := customProp then
+    unless ← isDefEq prop p do
+      throwError "istart: {p} is not a valid BI instance type"
+
   let P ← mkFreshExprMVarQ q($prop)
   let bi ← mkFreshExprMVarQ q(BI $prop)
-  let .some (_, mvars) ← ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal .out $prop .out $bi $P)
-    | throwError "istart: {goal} is not an emp valid"
+
+  let io : Q(InOut) := if customProp.isSome then q(.in) else q(.out)
+
+  let .some (inst, mvars) ←
+    ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal $io $prop .out $bi $P)
+  | throwError "istart: {goal} is not an emp valid"
   if !mvars.isEmpty then throwError "istart does not support creating mvars"
 
   let irisGoal := { u, prop, bi, hyps := .mkEmp bi, goal := P, .. }
   let subgoal : Quoted q(⊢ $P) ←
     mkFreshExprSyntheticOpaqueMVar (IrisGoal.toExpr irisGoal) (← mvar.getTag)
-  mvar.assign q(asEmpValid_2 $goal $subgoal)
+  mvar.assign q(asEmpValid_2 $goal $inst $subgoal)
   pure (subgoal.mvarId!, irisGoal)
 
 /-- Run a ProofModeM computation on the main goal, ordering resulting goals with dependencies last. -/
diff --git a/Iris/Iris/ProofMode/Tactics/Basic.lean b/Iris/Iris/ProofMode/Tactics/Basic.lean
index ce79fb78d..0797c1396 100644
--- a/Iris/Iris/ProofMode/Tactics/Basic.lean
+++ b/Iris/Iris/ProofMode/Tactics/Basic.lean
@@ -13,7 +13,7 @@ public meta import Iris.ProofMode.ProofModeM
 public meta section
 
 namespace Iris.ProofMode
-open Lean Elab.Tactic Meta Qq BI Std
+open Lean Elab.Tactic Meta Qq BI Std Lean.Elab Term
 
 /-- `itrivial` collects tactics to solve trivial Iris goals. It is used by the `//` specialization
 and introduction patterns. One can add new tactics using
@@ -44,6 +44,15 @@ elab "istart" : tactic => do
   let (mvar, _) ← startProofMode (← getMainGoal)
   replaceMainGoal [mvar]
 
+/--
+  `istart prop` starts the Iris Proof Mode with a specific `prop`.
+-/
+elab "istart " colGt prop:term : tactic => do
+  let mvar ← getMainGoal
+  let customProp ← mvar.withContext do elabType prop >>= (instantiateMVars ·)
+  let (mvar, _) ← startProofMode mvar (some customProp)
+  replaceMainGoal [mvar]
+
 /--
   `istop` stops the Iris Proof Mode by turning the goal back
   into plain entailment.

From 392c4a07bac035ad5d1090ff9169ccaf9ba6be18 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Wed, 8 Jul 2026 17:06:37 +0200
Subject: [PATCH 03/12] More specific error message for `istart`

---
 Iris/Iris/ProofMode/ProofModeM.lean | 26 ++++++++++++++------------
 1 file changed, 14 insertions(+), 12 deletions(-)

diff --git a/Iris/Iris/ProofMode/ProofModeM.lean b/Iris/Iris/ProofMode/ProofModeM.lean
index e56ec1d4b..e2ea8637f 100644
--- a/Iris/Iris/ProofMode/ProofModeM.lean
+++ b/Iris/Iris/ProofMode/ProofModeM.lean
@@ -136,19 +136,21 @@ def startProofMode (mvar : MVarId) (customProp : Option Expr := none) :
 
   let P ← mkFreshExprMVarQ q($prop)
   let bi ← mkFreshExprMVarQ q(BI $prop)
-
   let io : Q(InOut) := if customProp.isSome then q(.in) else q(.out)
-
-  let .some (inst, mvars) ←
-    ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal $io $prop .out $bi $P)
-  | throwError "istart: {goal} is not an emp valid"
-  if !mvars.isEmpty then throwError "istart does not support creating mvars"
-
-  let irisGoal := { u, prop, bi, hyps := .mkEmp bi, goal := P, .. }
-  let subgoal : Quoted q(⊢ $P) ←
-    mkFreshExprSyntheticOpaqueMVar (IrisGoal.toExpr irisGoal) (← mvar.getTag)
-  mvar.assign q(asEmpValid_2 $goal $inst $subgoal)
-  pure (subgoal.mvarId!, irisGoal)
+  let synthResult ← ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal $io $prop .out $bi $P)
+
+  match synthResult, customProp with
+  | .some (inst, mvars), _ =>
+    if !mvars.isEmpty then throwError "istart does not support creating mvars"
+    let irisGoal := { u, prop, bi, hyps := .mkEmp bi, goal := P, .. }
+    let subgoal : Quoted q(⊢ $P) ←
+      mkFreshExprSyntheticOpaqueMVar (IrisGoal.toExpr irisGoal) (← mvar.getTag)
+    mvar.assign q(asEmpValid_2 $goal $inst $subgoal)
+    pure (subgoal.mvarId!, irisGoal)
+  | _, none =>
+    throwError "istart: {goal} is not an emp valid"
+  | _, some _ =>
+    throwError "istart: {goal} is not an emp valid in {customProp}"
 
 /-- Run a ProofModeM computation on the main goal, ordering resulting goals with dependencies last. -/
 def ProofModeM.runTactic (x : MVarId → IrisGoal → ProofModeM α) (s : ProofModeM.State := {}) : TacticM α := do

From 5d7c8a1cdd8e3840b42521fd246a2883c1f8246c Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Wed, 8 Jul 2026 17:13:31 +0200
Subject: [PATCH 04/12] Code refactoring in `startProofMode`

---
 Iris/Iris/ProofMode/ProofModeM.lean | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/Iris/Iris/ProofMode/ProofModeM.lean b/Iris/Iris/ProofMode/ProofModeM.lean
index e2ea8637f..9c258eb38 100644
--- a/Iris/Iris/ProofMode/ProofModeM.lean
+++ b/Iris/Iris/ProofMode/ProofModeM.lean
@@ -116,23 +116,20 @@ def startProofMode (mvar : MVarId) (customProp : Option Expr := none) :
 
   -- check if already in proof mode
   if let some irisGoal := parseIrisGoal? goal then
-    match customProp with
-    | none =>
-      return (mvar, irisGoal)
-    | some customProp =>
+    customProp.forM <| fun customProp => do
       let eq ← isDefEq irisGoal.prop customProp
-      if !eq then
-        throwError "istart: currently in the Iris Proof Mode with {irisGoal.prop} rather than {customProp}"
-      return (mvar, irisGoal)
+      if !eq then throwError m!"istart: currently in the Iris Proof Mode with\
+        {irisGoal.prop} rather than {customProp}"
+    return (mvar, irisGoal)
 
   let some goal ← checkTypeQ goal q(Prop)
     | throwError "type mismatch\n{← mkHasTypeButIsExpectedMsg (← inferType goal) q(Prop)}"
   let u ← mkFreshLevelMVar
   let prop ← mkFreshExprMVarQ q(Type u)
 
-  if let some p := customProp then
-    unless ← isDefEq prop p do
-      throwError "istart: {p} is not a valid BI instance type"
+  customProp.forM <| fun customProp => do
+    let eq ← isDefEq prop customProp
+    if !eq then throwError "istart: {customProp} is not a valid BI instance type"
 
   let P ← mkFreshExprMVarQ q($prop)
   let bi ← mkFreshExprMVarQ q(BI $prop)

From d843263820d65a914dd5ca2cb2c1e43e963fc0ea Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Wed, 8 Jul 2026 17:14:03 +0200
Subject: [PATCH 05/12] Add tests for `istart`

---
 Iris/Iris/ProofMode/ProofModeM.lean |  2 +-
 Iris/Iris/Tests/Tactics.lean        | 40 ++++++++++++++++++++++++++++-
 2 files changed, 40 insertions(+), 2 deletions(-)

diff --git a/Iris/Iris/ProofMode/ProofModeM.lean b/Iris/Iris/ProofMode/ProofModeM.lean
index 9c258eb38..417ee9bd5 100644
--- a/Iris/Iris/ProofMode/ProofModeM.lean
+++ b/Iris/Iris/ProofMode/ProofModeM.lean
@@ -118,7 +118,7 @@ def startProofMode (mvar : MVarId) (customProp : Option Expr := none) :
   if let some irisGoal := parseIrisGoal? goal then
     customProp.forM <| fun customProp => do
       let eq ← isDefEq irisGoal.prop customProp
-      if !eq then throwError m!"istart: currently in the Iris Proof Mode with\
+      if !eq then throwError m!"istart: currently in the Iris Proof Mode with \
         {irisGoal.prop} rather than {customProp}"
     return (mvar, irisGoal)
 
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index fb8509a5f..dcef0f3a4 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -24,10 +24,48 @@ open BI CMRA DFrac
 example [BI PROP] (Q : PROP) (H : Q ⊢ Q) : Q ⊢ Q := by
   istart
   iintro _HQ
-  have HH: True := by trivial
+  have HH : True := by trivial
   istop
   exact H
 
+/-- Tests `istart` with a BI instance specified. -/
+example [BI PROP1] [BI PROP2] (P1 : PROP1) (P2 : PROP2)
+    (_ : ⊢@{PROP1} P1) : ⊢@{PROP2} P2 -∗ P2 := by
+  istart PROP2
+  iintro HP
+  iassumption
+
+/- Tests `istart` with the wrong BI instance specified. -/
+/-- error: istart: ⊢ P2 is not an emp valid in PROP1 -/
+#guard_msgs in
+example [BI PROP1] [BI PROP2] (P1 : PROP1) (P2 : PROP2)
+    (h : ⊢@{PROP1} P1) : ⊢@{PROP2} P2 := by
+  istart PROP1
+
+/- Tests `istart` with an invalid type specified as the BI instance. -/
+/-- error: istart: True is not a valid BI instance type -/
+#guard_msgs in
+example [BI PROP1] [BI PROP2] (P1 : PROP1) (P2 : PROP2)
+    (h : ⊢@{PROP1} P1) : ⊢@{PROP2} P2 := by
+  istart True
+
+/- Tests `istart` within the Iris Proof Mode. -/
+example [BI PROP1] [BI PROP2] (P1 : PROP1) (P2 : PROP2)
+    (_ : ⊢@{PROP1} P1) : ⊢@{PROP2} P2 -∗ P2 := by
+  iintro P2
+  istart PROP2
+  istart
+  istart PROP2
+  iassumption
+
+/- Tests `istart` within the Iris Proof Mode with the wrong BI instance specified. -/
+/-- error: istart: currently in the Iris Proof Mode with PROP2 rather than PROP1 -/
+#guard_msgs in
+example [BI PROP1] [BI PROP2] (P1 : PROP1) (P2 : PROP2)
+    (_ : ⊢@{PROP1} P1) : ⊢@{PROP2} P2 -∗ P2 := by
+  iintro P2
+  istart PROP1
+
 -- rename
 namespace rename
 

From 674afa4f8788efc4f7fbe8f653e9b3928036ffc9 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Wed, 8 Jul 2026 17:15:45 +0200
Subject: [PATCH 06/12] Update documentation

---
 Iris/Iris/ProofMode/Porting.lean | 2 +-
 Iris/tactics.md                  | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean
index dad0da8f9..3d0b32c9c 100644
--- a/Iris/Iris/ProofMode/Porting.lean
+++ b/Iris/Iris/ProofMode/Porting.lean
@@ -15,7 +15,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" missing "tactics"
 #rocq_concept proofmode "Tactics" "iSolveSideCondition" ported "iSolveSideconditionAt"
 #rocq_concept proofmode "Tactics" "iStartProof (basic)" ported "istart"
-#rocq_concept proofmode "Tactics" "iStartProof (with bi specified)" missing ""
+#rocq_concept proofmode "Tactics" "iStartProof (with bi specified)" ported "istart"
 #rocq_concept proofmode "Tactics" "iStopProof" ported "istop"
 #rocq_concept proofmode "Tactics" "iRename" ported "irename"
 #rocq_concept proofmode "Tactics" "iClear" ported "iclear"
diff --git a/Iris/tactics.md b/Iris/tactics.md
index f9e465ec0..409a71cb5 100644
--- a/Iris/tactics.md
+++ b/Iris/tactics.md
@@ -5,6 +5,7 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti
 ## Proof Mode Management
 
 - `istart` — Start the proof mode. (Most tactics start the proof mode automatically.)
+- `istart` *prop* — Start the proof mode, specifying the BI instance *prop*.
 - `istop` — Stop the proof mode, turning the goal back into a plain entailment.
 
 ## Context Management

From b5225ff4a80a35c9516356a447ededddd63f7dd0 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Wed, 8 Jul 2026 17:18:13 +0200
Subject: [PATCH 07/12] Minor update

---
 Iris/Iris/ProofMode/ProofModeM.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/ProofModeM.lean b/Iris/Iris/ProofMode/ProofModeM.lean
index 417ee9bd5..7cca9e5af 100644
--- a/Iris/Iris/ProofMode/ProofModeM.lean
+++ b/Iris/Iris/ProofMode/ProofModeM.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler, Zongyuan Liu, Yunsong Yang
+Authors: Michael Sammler, Zongyuan Liu, Yunsong Yang, Alvin Tang
 -/
 module
 

From f21ff6b0727dab908549a3a5a3496321c58d27af Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 21 Jul 2026 10:21:27 +0200
Subject: [PATCH 08/12] Syntax improvement: use `unless` and `if let some ...`

---
 Iris/Iris/ProofMode/ProofModeM.lean | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/Iris/Iris/ProofMode/ProofModeM.lean b/Iris/Iris/ProofMode/ProofModeM.lean
index 7cca9e5af..cf948c098 100644
--- a/Iris/Iris/ProofMode/ProofModeM.lean
+++ b/Iris/Iris/ProofMode/ProofModeM.lean
@@ -116,10 +116,9 @@ def startProofMode (mvar : MVarId) (customProp : Option Expr := none) :
 
   -- check if already in proof mode
   if let some irisGoal := parseIrisGoal? goal then
-    customProp.forM <| fun customProp => do
-      let eq ← isDefEq irisGoal.prop customProp
-      if !eq then throwError m!"istart: currently in the Iris Proof Mode with \
-        {irisGoal.prop} rather than {customProp}"
+    if let some customProp := customProp then
+      unless ← isDefEq irisGoal.prop customProp do
+        throwError m!"istart: currently in the Iris Proof Mode with {irisGoal.prop} rather than {customProp}"
     return (mvar, irisGoal)
 
   let some goal ← checkTypeQ goal q(Prop)
@@ -127,9 +126,9 @@ def startProofMode (mvar : MVarId) (customProp : Option Expr := none) :
   let u ← mkFreshLevelMVar
   let prop ← mkFreshExprMVarQ q(Type u)
 
-  customProp.forM <| fun customProp => do
-    let eq ← isDefEq prop customProp
-    if !eq then throwError "istart: {customProp} is not a valid BI instance type"
+  if let some customProp := customProp then
+    unless ← isDefEq prop customProp do
+      throwError "istart: {customProp} is not a valid BI instance type"
 
   let P ← mkFreshExprMVarQ q($prop)
   let bi ← mkFreshExprMVarQ q(BI $prop)

From 1902ba566c281786f3d244aa6e41278cfcfe59f0 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 21 Jul 2026 11:00:02 +0200
Subject: [PATCH 09/12] Port `AsEmpValid0` and `as_emp_valid_embed`

---
 Iris/Iris/ProofMode.lean                    |  1 +
 Iris/Iris/ProofMode/Classes.lean            |  5 ++++
 Iris/Iris/ProofMode/InstancesEmbedding.lean | 28 +++++++++++++++++++++
 3 files changed, 34 insertions(+)
 create mode 100644 Iris/Iris/ProofMode/InstancesEmbedding.lean

diff --git a/Iris/Iris/ProofMode.lean b/Iris/Iris/ProofMode.lean
index 399fffce4..9ae274987 100644
--- a/Iris/Iris/ProofMode.lean
+++ b/Iris/Iris/ProofMode.lean
@@ -6,6 +6,7 @@ public meta import Iris.ProofMode.Display
 public meta import Iris.ProofMode.Expr
 public import Iris.ProofMode.Instances
 public import Iris.ProofMode.InstancesCmra
+public import Iris.ProofMode.InstancesEmbedding
 public import Iris.ProofMode.InstancesFrame
 public import Iris.ProofMode.InstancesInternalEq
 public import Iris.ProofMode.InstancesLater
diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
index 567c182f1..278ff84ad 100644
--- a/Iris/Iris/ProofMode/Classes.lean
+++ b/Iris/Iris/ProofMode/Classes.lean
@@ -38,6 +38,11 @@ theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} {io : InOut}
     (φ : Prop) (inst : AsEmpValid .from φ io PROP .out bi P) : (⊢ P) → φ :=
   (AsEmpValid.as_emp_valid io .out).2 rfl
 
+@[ipm_class, rocq_alias AsEmpValid0]
+class AsEmpValid0 (d : AsEmpValid.Direction) (φ : Prop) (_ : InOut) (PROP : semiOutParam $ Type _)
+    (_ : InOut) (bi : semiOutParam $ BI PROP) (P : outParam PROP) where
+  as_emp_valid_0 : AsEmpValid d φ .in PROP .in bi P
+
 /- Depending on the use case, type classes with the prefix `From` or `Into` are used. Type classes
 with the prefix `From` are used to generate one or more propositions *from* which the original
 proposition can be derived. Type classes with the prefix `Into` are used to generate propositions
diff --git a/Iris/Iris/ProofMode/InstancesEmbedding.lean b/Iris/Iris/ProofMode/InstancesEmbedding.lean
new file mode 100644
index 000000000..5e3799569
--- /dev/null
+++ b/Iris/Iris/ProofMode/InstancesEmbedding.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 Alvin Tang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alvin Tang
+-/
+module
+
+public import Iris.BI
+public import Iris.ProofMode.Classes
+
+@[expose] public section
+
+namespace Iris.ProofMode
+open BI
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias as_emp_valid_embed]
+instance (priority := low) asEmpValid_embed
+    {PROP1 PROP2} [bi1 : BI PROP1] [bi2 : BI PROP2] [BiEmbed PROP1 PROP2]
+    (d : AsEmpValid.Direction) (φ : Prop) (P : PROP1)
+    [inst : AsEmpValid0 d φ io1 PROP1 io2 bi1 P] :
+    AsEmpValid d φ io1 PROP2 io2 bi2 (embed P) where
+  as_emp_valid := by
+    constructor
+    · intro hd hφ
+      apply (embed_emp_valid P).mpr <| inst.as_emp_valid_0.as_emp_valid.left hd hφ
+    · intro hd hP
+      apply inst.as_emp_valid_0.as_emp_valid.right hd <| (embed_emp_valid P).mp hP

From 7e855cb1c89344f7747ee6991e0454fa0cc9d53e Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 21 Jul 2026 11:37:11 +0200
Subject: [PATCH 10/12] Update type classes `AsEmpValid0` and its instances

---
 Iris/Iris/ProofMode/Classes.lean   |  7 +++++++
 Iris/Iris/ProofMode/Instances.lean | 15 ++++++++-------
 2 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
index 278ff84ad..d21c6c05c 100644
--- a/Iris/Iris/ProofMode/Classes.lean
+++ b/Iris/Iris/ProofMode/Classes.lean
@@ -43,6 +43,13 @@ class AsEmpValid0 (d : AsEmpValid.Direction) (φ : Prop) (_ : InOut) (PROP : sem
     (_ : InOut) (bi : semiOutParam $ BI PROP) (P : outParam PROP) where
   as_emp_valid_0 : AsEmpValid d φ .in PROP .in bi P
 
+@[ipm_backtrack, rocq_alias as_emp_valid_0]
+instance asEmpValid_of_0 (d : AsEmpValid.Direction) (φ : Prop) (io1 io2 : InOut)
+    PROP (bi : BI PROP) (P : PROP)
+    [inst : AsEmpValid0 d φ io1 PROP io2 bi P] :
+    AsEmpValid d φ io1 PROP io2 bi P where
+  as_emp_valid := inst.as_emp_valid_0.as_emp_valid
+
 /- Depending on the use case, type classes with the prefix `From` or `Into` are used. Type classes
 with the prefix `From` are used to generate one or more propositions *from* which the original
 proposition can be derived. Type classes with the prefix `Into` are used to generate propositions
diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index 1cd553fc1..98ca1b734 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -22,21 +22,22 @@ open Iris.BI Iris.Std
 @[rocq_alias as_emp_valid_emp_valid]
 instance (priority := default + 10) asEmpValidEmpValid
     [bi : BI PROP] d (P : PROP) :
-    AsEmpValid d (⊢ P) io1 PROP io2 bi P := ⟨by simp⟩
+    AsEmpValid0 d (⊢ P) io1 PROP io2 bi P where
+  as_emp_valid_0 := ⟨by simp⟩
 
 @[rocq_alias as_emp_valid_entails]
 instance asEmpValid_entails [bi : BI PROP] d (P Q : PROP)
-: AsEmpValid d (P ⊢ Q) io1 PROP io2 bi iprop(P -∗ Q) where
-  as_emp_valid := ⟨λ _ => entails_wand, λ _ => wand_entails⟩
+: AsEmpValid0 d (P ⊢ Q) io1 PROP io2 bi iprop(P -∗ Q) where
+  as_emp_valid_0 := ⟨λ _ => entails_wand, λ _ => wand_entails⟩
 
 instance asEmpValid_bientails [bi : BI PROP] (P Q : PROP)
-: AsEmpValid d (P ⊣⊢ Q) io1 PROP io2 bi iprop(P ∗-∗ Q) where
-  as_emp_valid := ⟨λ _ => equiv_wandIff, λ _ => wandIff_equiv⟩
+: AsEmpValid0 d (P ⊣⊢ Q) io1 PROP io2 bi iprop(P ∗-∗ Q) where
+  as_emp_valid_0 := ⟨λ _ => equiv_wandIff, λ _ => wandIff_equiv⟩
 
 @[rocq_alias as_emp_valid_equiv]
 instance asEmpValid_equiv [bi : BI PROP] (P Q : PROP)
-: AsEmpValid d (P ≡ Q) io1 PROP io2 bi iprop(P ∗-∗ Q) where
-  as_emp_valid := ⟨λ _ h => equiv_wandIff (equiv_iff.1 h), λ _ h => (equiv_iff.2 (wandIff_equiv h))⟩
+: AsEmpValid0 d (P ≡ Q) io1 PROP io2 bi iprop(P ∗-∗ Q) where
+  as_emp_valid_0 := ⟨λ _ h => equiv_wandIff (equiv_iff.1 h), λ _ h => (equiv_iff.2 (wandIff_equiv h))⟩
 
 @[rocq_alias as_emp_valid_forall]
 instance asEmpValid_forall {α} [bi : BI PROP] (Φ : α → Prop) (P : α → PROP)

From 11980e0a53804cdbcda8b3885da07039a01a328a Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 21 Jul 2026 11:37:28 +0200
Subject: [PATCH 11/12] Add more tests for `istart` with BI specified

---
 Iris/Iris/Tests/Tactics.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 19045fdbf..158c7f467 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -66,6 +66,29 @@ example [BI PROP1] [BI PROP2] (P1 : PROP1) (P2 : PROP2)
   iintro P2
   istart PROP1
 
+/- Tests `istart` with BI specified and embedding involved. -/
+example [BI PROP1] [BI PROP2] [BiEmbed PROP1 PROP2] (P Q : PROP1)
+    (h : ⊢@{PROP1} P -∗ Q) : ⊢@{PROP1} P -∗ Q := by
+  istart PROP2
+  ihave H := h
+  iexact H
+
+/- Tests `istart` with embedding involved but an invalid BI specified. -/
+/-- error: istart: ⊢ P1 is not an emp valid in PROP3 -/
+#guard_msgs in
+example [BI PROP1] [BI PROP2] [BI PROP3] [BiEmbed PROP1 PROP2]
+  [BiEmbed PROP2 PROP3] (P1 : PROP1)
+    (h : ⊢@{PROP1} P1) : ⊢@{PROP1} P1 := by
+  istart PROP3
+
+/- Tests `istart` to ensure embedding is not used unless a BI is specified. -/
+/-- error: istart: currently in the Iris Proof Mode with PROP1 rather than PROP2 -/
+#guard_msgs in
+example [BI PROP1] [BI PROP2] [BiEmbed PROP1 PROP2]
+    (P1 : PROP1) (h : ⊢@{PROP1} P1) : ⊢@{PROP1} P1 := by
+  istart
+  istart PROP2
+
 -- rename
 namespace rename
 

From db7100e0200e96a954793f190793b38b22925ed2 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 21 Jul 2026 11:43:44 +0200
Subject: [PATCH 12/12] Remove "stale" `rocq_alias` annotation

---
 Iris/Iris/ProofMode/Classes.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
index d21c6c05c..1e65e8de3 100644
--- a/Iris/Iris/ProofMode/Classes.lean
+++ b/Iris/Iris/ProofMode/Classes.lean
@@ -43,7 +43,8 @@ class AsEmpValid0 (d : AsEmpValid.Direction) (φ : Prop) (_ : InOut) (PROP : sem
     (_ : InOut) (bi : semiOutParam $ BI PROP) (P : outParam PROP) where
   as_emp_valid_0 : AsEmpValid d φ .in PROP .in bi P
 
-@[ipm_backtrack, rocq_alias as_emp_valid_0]
+/- Corresponds to the Rocq instance `as_emp_valid_0`. -/
+@[ipm_backtrack]
 instance asEmpValid_of_0 (d : AsEmpValid.Direction) (φ : Prop) (io1 io2 : InOut)
     PROP (bi : BI PROP) (P : PROP)
     [inst : AsEmpValid0 d φ io1 PROP io2 bi P] :