structure Iris.ProofMode.RemoveHyp {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (e : Q(«$prop»)) : Type

• e' : Q(«$prop»)
• hyps' : Hyps bi self.e'
• out : Q(«$prop»)
• out' : Q(«$prop»)
• p : Q(Bool)
• eq : unknown_1 =Q iprop(□?unknown_2 unknown_3)
• pf : Q(«$e» ⊣⊢ unknown_1 ∗ unknown_2)

instance Iris.ProofMode.instInhabitedRemoveHyp {a✝ : Lean.Level} {a✝¹ : Q(Type a✝)} {a✝² : Q(BI $a✝)} {a✝³ : Q($a✝)} : Inhabited (RemoveHyp a✝² a✝³)

Equations

• Iris.ProofMode.instInhabitedRemoveHyp = { default := { e' := default, hyps' := default, out := default, out' := default, p := default, eq := ⋯, pf := default } }

inductive Iris.ProofMode.RemoveHypCore {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (e : Q(«$prop»)) (α : Type) : Type

• none {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(«$prop»)} {α : Type} : RemoveHypCore bi e α
• one {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(«$prop»)} {α : Type} (a : α) (out' : Q(«$prop»)) (p : Q(Bool)) (eq : «$e» =Q iprop(□?«$p» «$out'»)) : RemoveHypCore bi e α
• main {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(«$prop»)} {α : Type} (a : α) : RemoveHyp bi e → RemoveHypCore bi e α

theorem Iris.ProofMode.remove_l {PROP : Type u_1} [BI PROP] {P P' Q R : PROP} (h : P ⊣⊢ P' ∗ R) : P ∗ Q ⊣⊢ (P' ∗ Q) ∗ R

theorem Iris.ProofMode.remove_r {PROP : Type u_1} [BI PROP] {P Q Q' R : PROP} (h : Q ⊣⊢ Q' ∗ R) : P ∗ Q ⊣⊢ (P ∗ Q') ∗ R

theorem Iris.ProofMode.intuitionistically_sep_dup {PROP : Type u_1} [BI PROP] {P : PROP} : □ P ⊣⊢ □ P ∗ □ P

def Iris.ProofMode.Hyps.removeCore {m : Type → Type u_1} {u : Lean.Level} {α : Type} [Monad m] {prop : Q(Type u)} (bi : Q(BI «$prop»)) (rp : Bool) (check : Lean.Name → Lean.Name → Q(Bool) → Q(«$prop») → m (Option α)) {e : Q(«$prop»)} : Hyps bi e → m (RemoveHypCore bi e α)

If rp is true, the hyp will be removed even if it is in the intuitionistic context.

Equations

• One or more equations did not get rendered due to their size.
• Iris.ProofMode.Hyps.removeCore bi rp check (Iris.ProofMode.Hyps.emp x_3) = pure Iris.ProofMode.RemoveHypCore.none

theorem Iris.ProofMode.sep_emp_rev {PROP : Type u_1} [BI PROP] {P : PROP} : P ⊣⊢ P ∗ emp

theorem Iris.ProofMode.emp_sep_rev {PROP : Type u_1} [BI PROP] {P : PROP} : P ⊣⊢ emp ∗ P

def Iris.ProofMode.Hyps.removeG {m : Type → Type u_1} {u : Lean.Level} {α : Type} [Monad m] {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(Prop)} (rp : Bool) (hyps : Hyps bi e) (check : Lean.Name → Lean.Name → Q(Bool) → Q(«$prop») → m (Option α)) : m (Option (α × RemoveHyp bi e))

Equations

• One or more equations did not get rendered due to their size.

def Iris.ProofMode.Hyps.remove {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(«$prop»)} (rp : Bool) (hyps : Hyps bi e) (uniq : Lean.Name) : RemoveHyp bi e

Equations

• One or more equations did not get rendered due to their size.