You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
def liftRel (R : α → β → Prop) (A : α → Prop) (B : β → Prop) : Prop :=
  (∀ a, A a → ∃ b, B b ∧ R a b) ∧ (∀ b, B b → ∃ a, A a ∧ R a b)

class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where
  Equiv P Q := P ⊣⊢ Q

entails_preorder : Preorder Entails
  equiv_iff {P Q : PROP} : (P ≡ Q) ↔ P ⊣⊢ Q := by admit /- proof elided -/

abbrev Relation (α : Type _) := α → α → Prop

class Reflexive (R : Relation α) where
  refl {x : α} : R x x

class Transitive (R : Relation α) where
  trans {x y z : α} : R x y → R y z → R x z

class Preorder (R : Relation α) extends Reflexive R, Transitive R

macro:max "iprop(" P:term " : " t:term ")" : term => `((iprop($P) : $t))

class NonExpansive [OFE α] [OFE β] (f : α → β) where
  ne : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → f x₁ ≡{n}≡ f x₂

class NonExpansive₂ [OFE α] [OFE β] [OFE γ] (f : α → β → γ) where
  ne : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → f x₁ y₁ ≡{n}≡ f x₂ y₂

@[ext] structure ContractiveHom (α β : Type _) [OFE α] [OFE β] extends Hom α β where
  [contractive : Contractive f]
  ne := ne_of_contractive f

instance OFE.Option.some.ne [OFE α] : OFE.NonExpansive (some : α → Option α) := ⟨fun _ _ _ => id⟩

instance Option.merge_ne [OFE α] {op : α → α → α} [NonExpansive₂ op] :
    NonExpansive₂ (Option.merge op) where
  ne n x1 x2 Hx y1 y2 Hy := by admit /- proof elided -/

structure Chain (α : Type _) [OFE α] where
  chain : Nat → α
  cauchy : n ≤ i → chain i ≡{n}≡ chain n

class IsCOFE (α : Type _) [OFE α] where
  compl : Chain α → α
  conv_compl {c : Chain α} : compl c ≡{n}≡ c n

instance OFE.ContractiveHom.fixpoint_ne [COFE α] [Inhabited α] :
    NonExpansive (ContractiveHom.fixpoint (α := α)) where
  ne n f1 f2 H := by admit /- proof elided -/

class Affine [BI PROP] (P : PROP) where
  affine : P ⊢ emp

class BIBase (PROP : Type u) where
  Entails : PROP → PROP → Prop
  emp : PROP
  pure : Prop → PROP
  and : PROP → PROP → PROP
  or : PROP → PROP → PROP
  imp : PROP → PROP → PROP
  sForall : (PROP → Prop) → PROP
  sExists : (PROP → Prop) → PROP
  sep : PROP → PROP → PROP
  wand : PROP → PROP → PROP
  persistently : PROP → PROP
  later : PROP → PROP

macro:25 P:term:29 " ⊢ " Q:term:25 : term => ``(BIBase.Entails iprop($P) iprop($Q))

delab_rule BIBase.Entails
  | `($_ $P $Q) => do ``($(← unpackIprop P) ⊢ $(← unpackIprop Q))

macro "∃" xs:explicitBinders ", " b:term : term => do
  return ⟨← expandExplicitBinders ``BIBase.exists xs b⟩

def wandIff [BIBase PROP] (P Q : PROP) : PROP := iprop((P -∗ Q) ∧ (Q -∗ P))

def affinely    [BIBase PROP] (P : PROP) : PROP := iprop(emp ∧ P)

def absorbingly [BIBase PROP] (P : PROP) : PROP := iprop(True ∗ P)

structure BiEntails [BIBase PROP] (P Q : PROP) where
  mp : P ⊢ Q
  mpr : Q ⊢ P

macro:25 P:term:29 " ⊣⊢ " Q:term:29 : term => ``(BiEntails iprop($P) iprop($Q))

delab_rule BIBase.Entails
  | `($_ iprop(emp) $P) => do ``(⊢ $(← unpackIprop P))

delab_rule BIBase.BiEntails
  | `($_ $P $Q) => do ``($(← unpackIprop P) ⊣⊢ $(← unpackIprop Q))

def intuitionistically [BIBase PROP] (P : PROP) : PROP := iprop(<affine> <pers> P)

def persistentlyIf [BIBase PROP] (p : Bool) (P : PROP) : PROP := iprop(if p then <pers> P else P)

def affinelyIf [BIBase PROP] (p : Bool) (P : PROP) : PROP := iprop(if p then <affine> P else P)

def absorbinglyIf [BIBase PROP] (p : Bool) (P : PROP) : PROP := iprop(if p then <absorb> P else P)

def intuitionisticallyIf [BIBase PROP] (p : Bool) (P : PROP) : PROP := iprop(if p then □ P else P)

def bigAnd [BIBase PROP] (Ps : List PROP) : PROP := bigOp and iprop(True) Ps

def bigOr [BIBase PROP] (Ps : List PROP) : PROP := bigOp or iprop(False) Ps

def bigSep [BIBase PROP] (Ps : List PROP) : PROP := bigOp sep iprop(emp) Ps

def bigOp (f : PROP → PROP → PROP) (unit : PROP) : List PROP → PROP
  | []      => unit
  | [P]     => P
  | P :: Ps => f P (bigOp f unit Ps)

class LawfulBigOp (f : PROP → PROP → PROP) (unit : outParam PROP)
    (eq : outParam (PROP → PROP → Prop)) where
  refl : eq a a
  symm : eq a b → eq b a
  trans : eq a b → eq b c → eq a c
  comm : eq (f a b) (f b a)
  assoc : eq (f (f a b) c) (f a (f b c))
  left_id : eq (f unit a) a
  congr_l : eq a a' → eq (f a b) (f a' b)

instance COFE.OFunctor.constOF_RFunctor [CMRA B] : RFunctor (constOF B) where
  map f g := by admit /- proof elided -/

instance intuitionistically_persistent [BI PROP] (P : PROP) : Persistent iprop(□ P) :=
  inferInstanceAs (Persistent iprop(<affine> _))

instance intoWand_imp_false [BI PROP] (P Q P' : PROP) [Absorbing P'] [Absorbing iprop(P' → Q)]
    [h : FromAssumption b P P'] : IntoWand false b iprop(P' → Q) P Q where
  into_wand := wand_intro <| (sep_mono_r h.1).trans <| by dsimp; exact sep_and.trans imp_elim_l

def Agree.map : CMRA.Hom (Agree α) (Agree β) where
  f := map' f
  ne := inferInstance
  validN {n x} hval := by admit /- proof elided -/

abbrev GenMap := α → Option β

Ne in Init.Core

class BIBUpdatePlainly (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIPlainly PROP] where
  bupd_plainly {P : PROP} : iprop((|==> ■ P)) ⊢ P

instance pure_persistent (φ : Prop) [BI PROP] : Persistent (PROP := PROP) iprop(⌜φ⌝) where
  persistent := persistently_pure.2

instance (priority := default + 30) fromAssumption_affinely_r [BI PROP] (P Q : PROP)
    [h : FromAssumption true P Q] : FromAssumption true P iprop(<affine> Q) where
  from_assumption := affinely_idem.2.trans <| affinely_mono h.1

instance fromPure_exists (a : Bool) [BI PROP] (Φ : α → PROP) (φ : α → Prop)
    [h : ∀ x, FromPure a iprop(Φ x) (φ x)] : FromPure a iprop(∃ x, Φ x) (∃ x, φ x) where
  from_pure := (affinelyIf_mono pure_exists.2).trans <|
    affinelyIf_exists.1.trans (exists_mono fun x => (h x).1)

instance intoWand_and_r (p q : Bool) [BI PROP] (R1 R2 P' Q' : PROP)
    [h : IntoWand p q R2 Q' P'] : IntoWand p q iprop(R1 ∧ R2) Q' P' where
  into_wand := (intuitionisticallyIf_mono and_elim_r).trans h.1

class RFunctor (F : COFE.OFunctorPre) where
  
  
  
  [cmra [OFE α] [OFE β] : CMRA (F α β)]
  map [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] :
    (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -C> F α₂ β₂
  map_ne [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] :
    NonExpansive₂ (@map α₁ α₂ β₁ β₂ _ _ _ _)
  map_id [OFE α] [OFE β] (x : F α β) : map (@Hom.id α _) (@Hom.id β _) x ≡ x
  map_comp [OFE α₁] [OFE α₂] [OFE α₃] [OFE β₁] [OFE β₂] [OFE β₃]
    (f : α₂ -n> α₁) (g : α₃ -n> α₂) (f' : β₁ -n> β₂) (g' : β₂ -n> β₃) (x : F α₁ β₁) :
    map (f.comp g) (g'.comp f') x ≡ map g g' (map f f' x)

instance fromOr_intuitionistically [BI PROP] (P Q1 Q2 : PROP) [h : FromOr P Q1 Q2] :
    FromOr iprop(□ P) iprop(□ Q1) iprop(□ Q2) where
  from_or := intuitionistically_or.2.trans (intuitionistically_mono h.1)

Or.inr in Init.Prelude

partial def handleDependentArrows {prop : Q(Type u)} (bi : Q(BI $prop)) (val : Expr) (goals : IO.Ref (Array MVarId)) : TacticM (Expr × Q(Prop)) := do
  let p : Q(Prop) ← inferType val
  if let .forallE _ binderType _ _ := p then
    let m ← mkFreshExprMVar binderType
    let val' := mkApp val m
    goals.modify (·.push m.mvarId!)
    return ← handleDependentArrows bi val' goals
  else
    return (val, p)

instance (priority := default + 20) fromAssumption_absorbingly_r (p : Bool) [BI PROP] (P Q : PROP)
    [h : FromAssumption p P Q] : FromAssumption p P iprop(<absorb> Q) where
  from_assumption := absorbingly_intro.trans <| absorbingly_mono h.1

Lean.Meta.saveState in Lean.Meta.Basic

instance emp_intuitionistic [BI PROP] : Intuitionistic iprop(emp : PROP) where
  intuitionistic := intuitionistically_emp.2

Qq.inferTypeQ in Qq.MetaM

Lean.Elab.Tactic.getMainGoal in Lean.Elab.Tactic.Basic

instance : CMRA (Agree α) where
  pcore := some
  op := Agree.op
  ValidN := Agree.validN
  Valid := Agree.valid

@[simp] def Heap.union [Heap T K V] : T → T → T := merge (fun v _ => v)

def Agree.valid (x : Agree α) : Prop := ∀ n, x.validN n

def Replaces [BI PROP] (K A B : PROP) := (B -∗ K) ⊢ (A -∗ K)

Or in Init.Prelude

protected def emp : UPred M where
  holds _ _ := True
  mono _ _ _ := trivial

instance intoOr_absorbingly [BI PROP] (P Q1 Q2 : PROP) [h : IntoOr P Q1 Q2] :
    IntoOr iprop(<absorb> P) iprop(<absorb> Q1) iprop(<absorb> Q2) where
  into_or := (absorbingly_mono h.1).trans absorbingly_or.1

Qq.checkTypeQ in Qq.MetaM

| .intuitionistic arg =>
    iCasesIntuitionistic bi P Q A' p fun B' =>
      iCasesCore hyps Q q(true) q(iprop(□ $B')) B' ⟨⟩ arg @k

Option.map in Init.Prelude

instance [BI PROP] : Idempotent (α := PROP) BiEntails and := ⟨and_self⟩

instance fromPure_pure_wand_true (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
    [h1 : IntoPure P1 φ1] [h2 : FromPure true P2 φ2] [Affine P1] :
    FromPure true iprop(P1 -∗ P2) (φ1 → φ2) where
  from_pure := by admit /- proof elided -/

instance : Trans Equiv (Included (α := α)) Included where
  trans := inc_of_eqv_of_inc

k in QqTest.matching

protected def Hom.comp [OFE α] [OFE β] [OFE γ] (g : β -n> γ) (f : α -n> β) : α -n> γ where
  f := g.f ∘ f.f
  ne.1 _ _ _ h := g.ne.1 (f.ne.1 h)

let Q1 ← mkFreshExprMVarQ prop
  let Q2 ← mkFreshExprMVarQ prop
  let _ ← synthInstanceQ q(FromSep $goal $Q1 $Q2)

protected def sep (P Q : UPred M) : UPred M where
  holds n x := ∃ x1 x2, x ≡{n}≡ x1 • x2 ∧ P n x1 ∧ Q n x2
  mono {n₁ n₂ m₁ m₂} := fun ⟨x₁, x₂, Hx, HP, HQ⟩ ⟨m, Hm⟩ Hn => by admit /- proof elided -/

instance or_absorbing [BI PROP] (P Q : PROP) [Absorbing P] [Absorbing Q] :
    Absorbing iprop(P ∨ Q) where
  absorbing := absorbingly_or.1.trans (or_mono absorbing absorbing)

def LocalUpdate [CMRA α] (x y : α × α) : Prop :=
  ∀n mz, ✓{n} x.1 → x.1 ≡{n}≡ x.2 •? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 •? mz

abbrev γ : GId FF1 := ⟨0, Nat.zero_lt_succ _⟩

abbrev State (Val : Type _) := Nat → StateResult Val

instance : BIAffine (UPred M) := ⟨by admit /- proof elided -/
⟩

instance intoPure_absorbingly [BI PROP] (P : PROP) (φ : Prop)
    [h : IntoPure P φ] : IntoPure iprop(<absorb> P) φ where
  into_pure := (absorbingly_mono h.1).trans absorbingly_pure.1

def Agree.op (x y : Agree α) : Agree α :=
  ⟨x.car ++ y.car, by admit /- proof elided -/
  ⟩

instance fromPure_persistently [BI PROP] (P : PROP) (a : Bool) (φ : Prop)
    [h : FromPure true P φ] : FromPure a iprop(<pers> P) φ where
  from_pure := affinelyIf_elim.trans <| persistently_pure.2.trans <|
    persistently_affinely.2.trans <| persistently_mono h.1

def goalTracker {P} (goals : IO.Ref (Array MVarId)) (name : Name) (hyps : Hyps bi P)
    (goal : Q($prop)) : MetaM Q($P ⊢ $goal) := do
  let m : Q($P ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
    IrisGoal.toExpr { prop, bi, hyps, goal, .. }
  m.mvarId!.setUserName name
  goals.modify (·.push m.mvarId!)
  pure m

class Idempotent (R : Relation α) (f : α → α → α) where
  idem {x : α} : R (f x x) x

instance intoOr_or [BI PROP] (P Q : PROP) : IntoOr iprop(P ∨ Q) P Q := ⟨.rfl⟩

instance instA (n) : COFE (A F n) := (A' F n).2

def upN {k} : ∀ n, A F k -n> A F (k + n)
  | 0 => .id
  | n+1 => (up F (k + n)).comp (upN n)

class RFunctorContractive (F : COFE.OFunctorPre) extends (RFunctor F) where
  map_contractive [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] :
    Contractive (Function.uncurry (@map α₁ α₂ β₁ β₂ _ _ _ _))

instance intoPure_pure_sep (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
    [h1 : IntoPure P1 φ1] [h2 : IntoPure P2 φ2] : IntoPure iprop(P1 ∗ P2) (φ1 ∧ φ2) where
  into_pure := (sep_mono h1.1 h2.1).trans <| sep_and.trans pure_and.1

instance (priority := default + 30) fromAssumption_persistently_r [BI PROP] (P Q : PROP)
    [h : FromAssumption true P Q] : FromAssumption true P iprop(<pers> Q) where
  from_assumption := (persistent (P := iprop(□ P))).trans (persistently_mono h.1)

class Discrete (α : Type _) [CMRA α] extends OFE.Discrete α where
  discrete_valid {x : α} : ✓{0} x → ✓ x

instance bupd_ne : OFE.NonExpansive (bupd : UPred M → UPred M) where
  ne n x1 x2 Hx m y Hm Hv := by admit /- proof elided -/

abbrev IProp := UPred (IResUR FF)

instance forall_persistent [BI PROP] [BIPersistentlyForall PROP] (Ψ : α → PROP)
    [h : ∀ x, Persistent (Ψ x)] : Persistent iprop(∀ x, Ψ x) :=
  sForall_persistent _ fun _ ⟨_, eq⟩ => eq ▸ h _

instance intoEmpValid_entails [BI PROP] (P Q : PROP) : IntoEmpValid (P ⊢ Q) iprop(P -∗ Q) where
  into_emp_valid := entails_wand

def addHypInfo (stx : Syntax) (name uniq : Name) (prop : Q(Type u)) (ty : Q($prop))
    (isBinder := false) : MetaM Unit := do
  let lctx ← getLCtx
  let ty := q(HypMarker $ty)
  addLocalVarInfo stx (lctx.mkLocalDecl ⟨uniq⟩ name ty) (.fvar ⟨uniq⟩) ty isBinder

instance {n : Nat} : Trans (IncludedN (α := α) n) (Dist n) (IncludedN n) where
  trans := incN_of_incN_of_dist

class Disjoint (α : Type u) where
  disjoint : α → α → Prop

partial def unpackIprop [Monad m] [MonadRef m] [MonadQuotation m] : Term → m Term
  | `(iprop($P))             => do `($P)
  | `($P:ident)              => do `($P)
  | `(?$P:ident)             => do `(?$P)
  | `(($P))                  => do `(($(← unpackIprop P)))
  | `($P $[ $Q]*)            => do ``($P $[ $Q]*)
  | `(if $c then $t else $e) => do
    let t ← unpackIprop t
    let e ← unpackIprop e
    `(if $c then $t else $e)
  | `(($P : $t))             => do ``(($(← unpackIprop P) : $t))
  | `($t)                    => `($t:term)

class HasHeapMap (T1 T2 : Type _) (K V1 V2 : outParam (Type _))
   [Store T1 K (Option V1)] [Store T2 K (Option V2)] where
  hhmap (f : K → V1 → Option V2) : T1 → T2
  hhmap_get (f : K → V1 → Option V2) : get (hhmap f t) k = (get t k).bind (f k)

instance entails_trans [BI PROP] : Trans (α := PROP) Entails Entails Entails where
  trans h1 h2 := h1.trans h2

Bool in Init.Prelude

class Exclusive (x : α) where
  exclusive0_l y : ¬✓{0} x • y

class Plainly (PROP : Type _) where
  plainly : PROP → PROP

macro:25 "⊢ " P:term:25 : term => ``(emp ⊢ $P)

instance [BI PROP] : RightId (α := PROP) BiEntails emp sep := ⟨sep_emp⟩

Lean.Elab.withInfoContext' in Lean.Elab.InfoTree.Main

instance : BIUpdate (UPred M) where
  intro {P} _ x _ HP _ _ Hn H := ⟨_, ⟨H, P.mono HP (CMRA.incN_refl x) Hn⟩⟩
  mono Himp n x Hx HP k yf Hn H := by admit /- proof elided -/

instance intoExists_absorbingly [BI PROP] (P : PROP) (Φ : α → PROP) [h : IntoExists P Φ] :
    IntoExists iprop(<absorb> P) (fun a => iprop(<absorb> (Φ a))) where
  into_exists := (absorbingly_mono h.1).trans absorbingly_exists.1

instance empty_cancelable : Cancelable (unit : α) where
  cancelableN {n w t} _ e := calc
    w ≡{n}≡ unit • w := unit_left_id.dist.symm
    _ ≡{n}≡ unit • t := e
    _ ≡{n}≡ t := unit_left_id.dist

if rule?.isSome then
        state.restore
        applyReflexivity goal

instance persistently_absorbing [BI PROP] (P : PROP) : Absorbing iprop(<pers> P) where
  absorbing := absorbingly_persistently.1

instance fromPure_forall (a : Bool) [BI PROP] (Φ : α → PROP) (φ : α → Prop)
    [h : ∀ x, FromPure a iprop(Φ x) (φ x)] : FromPure a iprop(∀ x, Φ x) (∀ x, φ x) where
  from_pure := (affinelyIf_mono pure_forall_2).trans <|
    affinelyIf_forall_1.trans (forall_mono fun x => (h x).1)

partial def Hyps.find? {u prop bi} (name : Name) :
    ∀ {s}, @Hyps u prop bi s → Option (Name × Q(Bool) × Q($prop))
  | _, .emp _ => none
  | _, .hyp _ name' uniq p ty _ => if name == name' then (uniq, p, ty) else none
  | _, .sep _ _ _ _ lhs rhs => rhs.find? name <|> lhs.find? name

class Contractive [OFE α] [OFE β] (f : α → β) where
  distLater_dist : DistLater n x y → f x ≡{n}≡ f y

return ⟨← `(irisGoalStx| $hyps.reverse* ⊢ $goal:term)⟩
where
  delabHypotheses {u prop bi s} (hyps : @Hyps u prop bi s)
      (acc : NameMap Nat × Array (TSyntax ``irisHyp)) :
      DelabM (NameMap Nat × Array (TSyntax ``irisHyp)) := do
    match hyps with
    | .emp _ => pure acc
    | .hyp _ name _ p ty _ =>
      let mut (map, acc) := acc
      let (idx, name') ← if let some idx := map.find? name then
        pure (idx + 1, name.appendAfter <| if idx == 0 then "✝" else "✝" ++ idx.toSuperscriptString)
      else
        pure (0, name)
      let stx ← if isTrue p then
        `(irisHyp| □$(mkIdent name') : $(← unpackIprop (← delab ty)))
      else
        `(irisHyp| ∗$(mkIdent name') : $(← unpackIprop (← delab ty)))
      pure (map.insert name idx, acc.push stx)
    | .sep _ _ _ _ lhs rhs => delabHypotheses lhs (← delabHypotheses rhs acc)

Lean.PrettyPrinter.Delaborator.Delab in Lean.PrettyPrinter.Delaborator.Basic

instance intoForall_forall [BI PROP] (Φ : α → PROP) : IntoForall iprop(∀ a, Φ a) Φ := ⟨.rfl⟩

def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop))
    {P} (hyps : Hyps bi P) (Q A' A1 A2 : Q($prop)) (p : Q(Bool))
    (inst : Option Q(IntoAnd $p $A' $A1 $A2))
    (k : ∀ {P}, Hyps bi P → MetaM Q($P ⊢ $Q))
    (k1 k2 : ∀ {P}, Hyps bi P → (Q B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) →
      (∀ {P}, Hyps bi P → MetaM Q($P ⊢ $Q)) → MetaM Q($P ∗ $B ⊢ $Q)) :
    MetaM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
  if p.constName! == ``true then
    let some _ := inst | _ ← synthInstanceQ q(IntoAnd $p $A' $A1 $A2); unreachable!
    have : $p =Q true := ⟨⟩
    let Q' := q(iprop(□ $A2 -∗ $Q))
    let pf ← k1 hyps Q' q(iprop(□ $A1)) A1 ⟨⟩ fun hyps => do
      let pf ← k2 hyps Q q(iprop(□ $A2)) A2 ⟨⟩ k
      return q(wand_intro $pf)
    return q(and_elim_intuitionistic (A := $A') $pf)
  else
    let _ ← synthInstanceQ q(IntoSep $A' $A1 $A2)
    have : $p =Q false := ⟨⟩
    let Q' := q(iprop($A2 -∗ $Q))
    let pf ← k1 hyps Q' A1 A1 ⟨⟩ fun hyps => do
      let pf ← k2 hyps Q A2 A2 ⟨⟩ k
      return q(wand_intro $pf)
    return q(sep_elim_spatial (A := $A') $pf)

class IntoSep [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
  into_sep : P ⊢ Q1 ∗ Q2

instance asEmpValid2_entails [BI PROP] (P Q : PROP) : AsEmpValid2 (P ⊢ Q) iprop(P -∗ Q) :=
  AsEmpValid1.to2

Equiv in Mathlib.Logic.Equiv.Defs

def mkNameAnnotation (name uniq : Name) (e : Expr) : Expr :=
  .mdata ⟨[(nameAnnotation, .ofName name), (uniqAnnotation, .ofName uniq)]⟩ e

instance intoSep_intuitionistically_affine [BI PROP] (P Q1 Q2 : PROP) [h : IntoSep P Q1 Q2]
    [TCOr (Affine Q1) (Absorbing Q2)] [TCOr (Affine Q2) (Absorbing Q1)] :
    IntoSep iprop(□ P) iprop(□ Q1) iprop(□ Q2) where
  into_sep := (intuitionistically_mono <| h.1.trans sep_and).trans <|
    intuitionistically_and.1.trans and_sep_intuitionistically.1

instance intoSep_sep [BI PROP] (P Q : PROP) : IntoSep iprop(P ∗ Q) P Q := ⟨.rfl⟩

instance intoPure_affinely [BI PROP] (P : PROP) (φ : Prop)
    [h : IntoPure P φ] : IntoPure iprop(<affine> P) φ where
  into_pure := affinely_elim.trans h.1

@[simp]
def intuitionistic_action_spec (M : PROP1 → PROP2) : Prop :=
  match s with
  | .isEmpty => True
  | .forall Hconv C =>
      (∀ P, C P → iprop(□ P) ⊢ Hconv ▸ M iprop(□ P)) ∧
      (∀ P Q, iprop(M P ∧ M Q) ⊢ M iprop(P ∧ Q))
  | .transform C =>
      (∀ P Q, C P Q → iprop(□ P) ⊢ M iprop(□ Q)) ∧
      (∀ P Q, iprop(M P ∧ M Q) ⊢ M iprop(P ∧ Q))
  | .clear => True
  | .id H => ∀ P, iprop(□ P) ⊢ M (H ▸ iprop(□ P))

instance (priority := default - 10) fromSep_sep [BI PROP] (P1 P2 : PROP) :
    FromSep iprop(P1 ∗ P2) P1 P2 := ⟨.rfl⟩

instance : IsModal (PROP1 := PROP) intuitionistically (.id rfl) .isEmpty where
  spec_intuitionistic _ := intuitionistic
  spec_spatial := trivial
  emp := intuitionistic
  mono := (intuitionistically_mono ·)
  sep := intuitionistically_sep_2

def const [OFE α] (a : α) : Chain α where
  chain := fun _ => a
  cauchy _ := OFE.Dist.rfl

EmptyCollection.emptyCollection in Init.Core

abbrev HeapProp (Val : Type _) := State Val → Prop

instance later_absorbing [BI PROP] {P : PROP} [Absorbing P] : Absorbing iprop(▷ P) where
  absorbing := later_absorbingly.mpr.trans <| later_mono absorbing

private def matchAlts' := leading_parser matchAlts

instance fromAffinely_self [BI PROP] (P : PROP) : FromAffinely P P false := ⟨.rfl⟩

protected def sForall (Ψ : UPred M → Prop) : UPred M where
  holds n x := ∀ p, Ψ p → p n x
  mono a a_1 a_2 p a_3 := p.mono (a p a_3) a_1 a_2

Lean.MVarId in Lean.Expr

instance (priority := default + 10) fromSep_absorbingly [BI PROP] (P Q1 Q2 : PROP)
    [h : FromSep P Q1 Q2] : FromSep iprop(<absorb> P) iprop(<absorb> Q1) iprop(<absorb> Q2) where
  from_sep := absorbingly_sep.2.trans (absorbingly_mono h.1)

instance intoPure_intuitionistically [BI PROP] (P : PROP) (φ : Prop)
    [h : IntoPure P φ] : IntoPure iprop(□ P) φ where
  into_pure := intuitionistically_elim.trans h.1

instance cmraUnit : CMRA Unit where
  pcore _ := some ()
  op _ _ := ()
  ValidN _ _ := True
  Valid _ := True
  op_ne.ne _ _ _ := id
  pcore_ne _ _ := ⟨(), rfl, .rfl⟩
  validN_ne _ := id
  valid_iff_validN := ⟨fun _ _ => ⟨⟩, fun _ => ⟨⟩⟩
  validN_succ := id
  validN_op_left := id
  assoc := .rfl
  comm := .rfl
  pcore_op_left _ := .rfl
  pcore_idem _ := .rfl
  pcore_op_mono _ _ := ⟨.unit, .rfl⟩
  extend _ _ := ⟨(), (), .rfl, .rfl, .rfl⟩

def Update [CMRA α] (x y : α) := ∀ n mz,
  ✓{n} (x •? mz) → ✓{n} (y •? mz)

instance intoSep_pure (φ ψ : Prop) [BI PROP] :
    IntoSep (PROP := PROP) iprop(⌜φ ∧ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝) where
  into_sep := pure_and.2.trans persistent_and_sep_1

instance : OFE Unit where
  Equiv _ _ := True
  Dist _ _ _ := True
  dist_eqv := ⟨fun _ => ⟨⟩, id, fun _ => id⟩
  equiv_dist := by admit /- proof elided -/

@[simp] def optionValid : Option α → Prop
  | some x => ✓ x
  | none => True

instance [u : U] : TCIte (no_index false) T U := TCIte.e (u := u)

instance emp_affine [BI PROP] : Affine (PROP := PROP) iprop(emp) where
  affine := .rfl

def IResUR : Type := (i : GId FF) → GName → Option (FF[i] (iPrePropO FF) (iPrePropO FF))

class UCMRA (α : Type _) extends CMRA α where
  unit : α
  unit_valid : ✓ unit
  unit_left_id : unit • x ≡ x
  pcore_unit : pcore unit ≡ some unit

def op? [CMRA α] (x : α) : Option α → α
  | some y => x • y
  | none => x

instance {α : Type _} : OFE.Discrete (LeibnizO α) := ⟨congrArg id⟩

abbrev FF1 : GFunctors := #[COFE.constOF (Agree (LeibnizO String))]

macro "%" pat:icasesPat : icasesPat => `(icasesPat| ⌜$pat⌝)

instance asEmpValid2_equiv [BI PROP] (P Q : PROP) : AsEmpValid2 (P ⊣⊢ Q) iprop(P ∗-∗ Q) :=
  AsEmpValid1.to2

instance : OFE.NonExpansive (BUpd.bupd (PROP := UPred M)) := bupd_ne

Union in Init.Core

instance {ma : Option α} [∀ a : α, IdFree a] [∀ a : α, Cancelable a] : Cancelable ma :=

Lean.Elab.Tactic.TacticM in Lean.Elab.Tactic.Basic

class NumericFraction (α : Type _) extends One α, Add α, LE α, LT α where
  add_comm : ∀ a b : α, a + b = b + a
  add_assoc : ∀ a b c : α, a + (b + c) = (a + b) + c
  add_left_cancel : ∀ {a b c : α}, a + b = a + c → b = c
  le_def : ∀ {a b : α}, a ≤ b ↔ a = b ∨ a < b
  lt_def : ∀ {a b : α}, a < b ↔ ∃ c : α, a + c = b
  lt_irrefl : ∀ {a : α}, ¬a < a

instance [CMRA A] : OFE.NonExpansive (cmraValid : A → UPred M) where
  ne _ _ _ H _ _ Hn _ := (H.le Hn).validN

assoc : op x (op y z) ≡ op (op x y) z
  comm : op x y ≡ op y x

class CMRA (α : Type _) extends OFE α where
  pcore : α → Option α
  op : α → α → α
  ValidN : Nat → α → Prop
  Valid : α → Prop

-- A proof with no resources
example (P Q : IProp FF0) : P ∗ Q ⊢ ⌜True⌝ :=

class IntoOr [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
  into_or : P ⊢ Q1 ∨ Q2

| .disjunction (arg :: args) =>
    iCasesOr bi P Q A' p
      (iCasesCore hyps Q p · · · arg @k)
      (iCasesCore hyps Q p · · · (.disjunction args) @k)

@[simp] instance [NumericFraction T] : LE (Frac T) := ⟨(·.1 ≤ ·.1)⟩

instance URFunctorContractive.toRFunctorContractive
    [URFunctorContractive F] : RFunctorContractive F where
  map_contractive := map_contractive

instance [Heap T K V] [OFE V] (op : V → V → V) [NonExpansive₂ op] :
    NonExpansive₂ (merge (T := T) op) where
  ne _ {_ _} Ht {_ _} Hs k := by admit /- proof elided -/

instance asEmpValid1_equiv [BI PROP] (P Q : PROP) : AsEmpValid1 (P ⊣⊢ Q) iprop(P ∗-∗ Q) where
  as_emp_valid := ⟨equiv_wandIff, wandIff_equiv⟩

instance {a : α} [IdFree a] [Cancelable a] : Cancelable (some a) :=

return rule?.isNone
    else
      
      applyReflexivity goal
      return false
</all_available_defs>

<all_available_lemmas>
theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R

theorem BIBase.BiEntails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊣⊢ Q) (h2 : Q ⊣⊢ R) : P ⊣⊢ R

@[simp, refl] theorem Dist.rfl [OFE α] {n} {x : α} : x ≡{n}≡ x

@[symm] theorem Dist.symm [OFE α] {n} {x : α} : x ≡{n}≡ y → y ≡{n}≡ x

theorem Dist.trans [OFE α] {n} {x : α} : x ≡{n}≡ y → y ≡{n}≡ z → x ≡{n}≡ z

theorem equiv_eqv [ofe : OFE α] : Equivalence ofe.Equiv

theorem Equiv.trans [OFE α] {x : α} : x ≡ y → y ≡ z → x ≡ z

theorem DistLater.trans [OFE α] {n} {x : α} (h1 : DistLater n x y) (h2 : DistLater n y z) :
    DistLater n x z

theorem _root_.Iris.OFE.Equiv.core : ∀ {x₁ x₂ : α}, x₁ ≡ x₂ → core x₁ ≡ core x₂

theorem cancelable_iff {x₁ x₂ : α} (e : x₁ ≡ x₂) : Cancelable x₁ ↔ Cancelable x₂

theorem affinely_sep [BI PROP] [BIPositive PROP] {P Q : PROP} :
    <affine> (P ∗ Q) ⊣⊢ <affine> P ∗ <affine> Q

theorem absorbingly_persistently [BI PROP] {P : PROP} : <absorb> <pers> P ⊣⊢ <pers> P

theorem fixpoint_unique [COFE α] [Inhabited α] {f : α -c> α} {x : α} (H : x ≡ f x) :
    x ≡ fixpoint f

@[simp] theorem persistentlyIf_false [BI PROP] (P : PROP) : iprop(<pers>?false P) = P

theorem spatial_elim_intuitionistic [BI PROP] {A A' Q : PROP} [FromAffinely A' A true]
    (h : P ∗ A' ⊢ Q) : P ∗ □ A ⊢ Q

theorem UpdateP.discrete_total [CMRA.Discrete α] [CMRA.IsTotal α] :
    x ~~>: P ↔ ∀ (z : α), ✓ (x • z) → ∃ y, P y ∧ ✓ (y • z)

theorem from_forall_intro [BI PROP] {P Q : PROP} {Φ : α → PROP} [inst : FromForall Q Φ]
    (h : ∀ a, P ⊢ Φ a) : P ⊢ Q

theorem sep_comm [BI PROP] {P Q : PROP} : P ∗ Q ⊣⊢ Q ∗ P

theorem id_freeN_r {n n'} {x : α} [IdFree x] {y} (v : ✓{n} x) : ¬(x • y ≡{n'}≡ x)

theorem intuitionistically_true [BI PROP] : □ True ⊣⊢ (emp : PROP)

theorem and_assoc [BI PROP] {P Q R : PROP} : (P ∧ Q) ∧ R ⊣⊢ P ∧ Q ∧ R

theorem LocalUpdate.core_id (x y z : α) [CMRA.CoreId y] (inc : y ≼ x) : (x, z) ~l~> (x, z • y)

theorem false_and [BI PROP] {P : PROP} : False ∧ P ⊣⊢ False

theorem Cancelable.of_eqv {x₁ x₂ : α} (e : x₁ ≡ x₂) (h : Cancelable x₁) : Cancelable x₂

@[rw_mono_rule]
theorem persistentlyIf_congr {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) :
    <pers>?p P ⊣⊢ <pers>?p Q

theorem intuitionisticallyIf_sep {p : Bool} [BI PROP] [BIPositive PROP] {P Q : PROP} :
    □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q

theorem plainly_and_emp_elim : emp ∧ ■ P ⊢ P

theorem plainly_forall {Ψ : α → PROP} : ■ (∀ a, Ψ a) ⊣⊢ ∀ a, ■ (Ψ a)

theorem CoreId.of_pcore_eq_some {x y : α} (e : pcore x = some y) : CoreId y

theorem point_valid_iff : ✓ (point i x : T) ↔ ✓ x

theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP}
    (h_rem : P ⊣⊢ P' ∗ □ A) (h : P' ⊢ Q) : P ⊢ Q

theorem incN_of_incN_le {n n'} {x y : α} (l1 : n' ≤ n) : x ≼{n} y → x ≼{n'} y

theorem f [BI PROP] : ⊢ (∃ (_x : Nat), True ∨ False : PROP)

theorem le_trans {a b c : α} : a ≤ b → b ≤ c → a ≤ c

theorem fixpoint_unfold [COFE α] [Inhabited α] (f : α -c> α) :
    fixpoint f ≡ f (fixpoint f)

protected theorem Tower.downN (X : Tower F) : ∀ i, downN F i (X (k+i)) ≡ X k

theorem imp_wand_persistently_2 [BI PROP] {P Q : PROP} : (<pers> P -∗ Q) ⊢ (<pers> P → Q)

theorem affinely_intro' [BI PROP] {P Q : PROP} (h : P ⊢ <affine> Q) :
    <affine> P ⊢ <affine> Q

theorem cancelable {x y z : α} [Cancelable x] (v : ✓(x • y)) (e : x • y ≡ x • z) : y ≡ z

theorem plainly_persistently_elim : ■ <pers> P ⊣⊢ ■ P

theorem sep_congr_r [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : P ∗ Q ⊣⊢ P ∗ Q'

theorem opM_opM_assoc {x : α} {y z : Option α} : (x •? y) •? z ≡ x •? (y • z)

theorem Update.transP {x y : α} (uxy : x ~~> y) (uyq : y ~~>: Q) : x ~~>: Q

theorem Update.equiv_right {x y z : α} (e : y ≡ z) (u : x ~~> y) : x ~~> z

theorem rename_twice [BI PROP] (Q : PROP) : Q ⊢ Q

theorem IsoFunStore.ext [Store T K V] [IsoFunStore T K V] {t1 t2 : T}
    (H : ∀ k, get t1 k = get t2 k) : t1 = t2

theorem set_eq_point_op_point [IsoFunStore T K (Option V)] {m : T} (Hemp : get m i = none) :
    set m i x = point i x • m

theorem core_incN_core {n} {x y : α} (inc : x ≼{n} y) : core x ≼{n} core y

theorem intuitionisticallyIf_idem {p : Bool} [BI PROP] {P : PROP} : □?p □?p P ⊣⊢ □?p P

theorem apply_forall [BI PROP] (P Q : α → PROP) (a b : α) (H : ⊢ ∀ x, ∀ y, P x -∗ Q y) : P a ⊢ Q b

theorem comm_L {x y : α} : x • y = y • x

theorem sep_emp_rev [BI PROP] {P : PROP} : P ⊣⊢ P ∗ emp

theorem persistently_idem [BI PROP] {P : PROP} : <pers> <pers> P ⊣⊢ <pers> P

theorem move_twice [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q

theorem or_assoc [BI PROP] {P Q R : PROP} : (P ∨ Q) ∨ R ⊣⊢ P ∨ Q ∨ R

theorem remove_l [BI PROP] {P P' Q R : PROP} (h : P ⊣⊢ P' ∗ R) :
    P ∗ Q ⊣⊢ (P' ∗ Q) ∗ R

theorem affinelyIf_sep {p : Bool} [BI PROP] [BIPositive PROP] {P Q : PROP} :
    <affine>?p (P ∗ Q) ⊣⊢ <affine>?p P ∗ <affine>?p Q

theorem imp_mono_r [BI PROP] {P Q Q' : PROP} (h : Q ⊢ Q') : (P → Q) ⊢ (P → Q')

theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop}
    [hA : IntoPure A φ] [or : TCOr (Affine A) (Absorbing Q)]
    (h : P ⊣⊢ P' ∗ A) (h_entails : φ → P' ⊢ Q) : P ⊢ Q :=
  h.1.trans <| match or with

theorem pcore_idem' {x : α} {cx} (e : pcore x ≡ some cx) : pcore cx ≡ some cx

theorem apply [BI PROP] (P Q : PROP) : ⊢ P -∗ (P -∗ Q) -∗ Q

theorem or_eq_ite [BI PROP] {P Q : PROP} : P ∨ Q ⊣⊢ ∃ (b : Bool), if b then P else Q

theorem split_rs [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ Q1 ∗ (P ∗ Q2)

theorem absorbinglyIf_sep_l {p : Bool} [BI PROP] {P Q : PROP} :
    <absorb>?p P ∗ Q ⊣⊢ <absorb>?p (P ∗ Q)

@[rw_mono_rule]
theorem imp_mono [BI PROP] {P P' Q Q' : PROP} (h1 : Q ⊢ P) (h2 : P' ⊢ Q') : (P → P') ⊢ Q → Q'

theorem ownM_op (m1 m2 : M) : ownM (m1 • m2) ⊣⊢ ownM m1 ∗ ownM m2

theorem multiple_intuitionistic [BI PROP] (P Q R : PROP) : ⊢ □ P -∗ Q -∗ □ (P -∗ Q -∗ □ R) -∗ R

theorem wand_iff_exists_persistently [BI PROP] [BIAffine PROP] {P Q : PROP} :
    (P -∗ Q) ⊣⊢ ∃ R, R ∗ <pers> (P ∗ R → Q)

theorem excl_map_ne [OFE α] [OFE β] (f : α -n> β) : NonExpansive (map f)

theorem intuitionisticallyIf_comm' {p q : Bool} [BI PROP] {P : PROP} :
    □?p □?q P ⊣⊢ □?q □?p P

theorem absorbinglyIf_sep_lr {p : Bool} [BI PROP] {P Q : PROP} :
    <absorb>?p P ∗ Q ⊣⊢ P ∗ <absorb>?p Q

theorem le_rfl {a : α} : a ≤ a

theorem multiple_lean' [BI PROP] (P Q R : PROP) (H : P ∗ Q ⊢ R) (HP : ⊢ P) : ⊢ Q -∗ R

theorem move_to_intuitionistic_and_back_disjunction [BI PROP] (Q : PROP) : ⊢ □ (Q ∨ Q) -∗ Q

theorem validN_fst {n} {x : α × β} (h : ✓{n} x) : ✓{n} x.fst

theorem split_ss [BI PROP] {P Q P1 P2 Q1 Q2 : PROP}
    (h1 : P ⊣⊢ P1 ∗ P2) (h2 : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P1 ∗ Q1) ∗ (P2 ∗ Q2)

theorem some_inc_some_of_dist_opM {mz : Option α} (H : x ≡{n}≡ y •? mz) : some y ≼{n} some x

protected theorem Hom.monoN [CMRA β] (f : α -C> β) n {x₁ x₂ : α} : x₁ ≼{n} x₂ → f x₁ ≼{n} f x₂

theorem Update.op_l {x y : α} : x • y ~~> x

theorem wand_intuitionistic_required_spatial [BI PROP] (Q : PROP) : □ P ⊢ (□ P -∗ Q) -∗ Q

theorem and_congr_r [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : P ∧ Q ⊣⊢ P ∧ Q'

theorem plainly_and_sep_r : P ∧ ■ Q ⊣⊢ P ∗ ■ Q

theorem _root_.Iris.OFE.Dist.validN : (x : α) ≡{n}≡ y → (✓{n} x ↔ ✓{n} y)

theorem forall_ne [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ≡{n}≡ Ψ a) :
    iprop(∀ a, Φ a) ≡{n}≡ iprop(∀ a, Ψ a)

theorem inc_op_left (x y : α) : x ≼ x • y

theorem true_sep_2 [BI PROP] {P : PROP} : P ⊢ True ∗ P

theorem affine [BI PROP] [BIAffine PROP] (P Q : PROP) : ⊢ (P → Q) -∗ <pers> P -∗ Q

theorem intuitionistically_false [BI PROP] : □ False ⊣⊢ (False : PROP)

theorem multiple_intuitionistic [BI PROP] (Q : PROP) : ⊢ □ P -∗ □ Q -∗ Q

theorem move_to_pure_conjunction [BI PROP] (Q : PROP) : ⊢ <affine> ⌜φ⌝ ∗ Q -∗ Q

theorem wandIff_congr_l [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : (P ∗-∗ Q) ⊣⊢ (P' ∗-∗ Q)

theorem forall_spatial_multiple [BI PROP] (Q : Nat → Nat → PROP) :
    ⊢ (∀ x, ∀ y, Q x y) -∗ Q x y

theorem coreId_iff_core_eq_self {x : α} [IsTotal α] : CoreId x ↔ core x = x

theorem imp_congr_r [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P → Q) ⊣⊢ (P → Q')

protected theorem Hom.core [CMRA β] (f : α -C> β) {x : α} : core (f x) ≡ f (core x)

theorem op_core_L {x : α} [IsTotal α] : x • core x = x

theorem impl_wand_plainly_2 : (■ P -∗ Q) ⊢ (■ P → Q)

theorem IncludedN.validN {n} {x y : α} : x ≼{n} y → ✓{n} y → ✓{n} x

theorem sep_elim_r [BI PROP] {P Q : PROP} [TCOr (Affine P) (Absorbing Q)] : P ∗ Q ⊢ Q

theorem inc_dom_inc {m1 m2 : T} (Hinc : m1 ≼ m2) : Set.Included (dom m1) (dom m2)

theorem set_equiv_point_op_point {m : T} (Hemp : get m i = none) : Equiv (set m i x) (point i x • m)

theorem conjunction_and_disjunction [BI PROP] [BIAffine PROP] (Q : PROP) :
    (P11 ∨ P12 ∨ P13) ∗ P2 ∗ (P31 ∨ P32 ∨ P33) ∗ Q ⊢ Q

theorem discrete_cancelable {x : α} [Discrete α]
    (H : ∀ {y z : α}, ✓(x • y) → x • y ≡ x • z → y ≡ z) : Cancelable x

theorem UpdateP.option' (P : α → Prop) (x : α) (uxp : x ~~>: P) : some x ~~>: Option.rec False P

theorem Hom.comp_assoc [OFE α] [OFE β] [OFE γ] [OFE δ]
    (h : γ -n> δ) (g : β -n> γ) (f : α -n> β) : (h.comp g).comp f = h.comp (g.comp f)

theorem core_op_mono (x y : α) : core x ≼ core (x • y)

theorem LocalUpdate.valid [CMRA.Discrete α] {x y x' y' : α}
    (h : ✓ x → ✓ y → some y ≼ some x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y')

theorem plainly_sep [BIPositive PROP] : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q

theorem _root_.Iris.OFE.Dist.op_l {x y z : α} : x ≡{n}≡ y → x • z ≡{n}≡ y • z

theorem conjunction_clear [BI PROP] [BIAffine PROP] (Q : PROP) : Q ∗ P ⊢ Q

theorem lean_pure [BI PROP] (Q : PROP) : <affine> ⌜⊢ Q⌝ ⊢ Q

theorem move_to_intuitionistic [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q

theorem valid0_of_validN {n} {x : α} : ✓{n} x → ✓{0} x

@[simp] theorem distLater_zero [OFE α] {x y : α} : DistLater 0 x y

theorem BIBase.Entails.of_eq [BI PROP] {P Q : PROP} (h : P = Q) : P ⊢ Q

theorem validN_op_right {n} {x y : α} : ✓{n} (x • y) → ✓{n} y

theorem affinelyIf_and_lr {p : Bool} [BI PROP] {P Q : PROP} :
    <affine>?p P ∧ Q ⊣⊢ P ∧ <affine>?p Q

theorem incN_op_left (n) (x y : α) : x ≼{n} x • y

theorem persistentlyIf_or {p : Bool} [BI PROP] {P Q : PROP} :
    <pers>?p (P ∨ Q) ⊣⊢ <pers>?p P ∨ <pers>?p Q

theorem pure [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ ⌜φ⌝ -∗ Q -∗ Q

theorem pure_elim_l [BI PROP] {φ : Prop} {Q R : PROP} (h : φ → Q ⊢ R) : ⌜φ⌝ ∧ Q ⊢ R

@[refl] theorem Included.rfl {x : α} : x ≼ x

theorem intuitionistically_plainly : □ ■ P ⊢ ■ □ P

theorem Agree.toAgree_inj {a b : α} : toAgree a ≡ toAgree b → a ≡ b

theorem disjoint_op_equiv_union {m1 m2 : T} (Hd : Set.Disjoint (dom m1) (dom m2)) :
    Equiv (m1 • m2) (union m1 m2)

theorem _root_.Iris.OFE.Dist.idFree {x₁ x₂ : α} (e : x₁ ≡{n}≡ x₂) : IdFree x₁ ↔ IdFree x₂

theorem persistentlyIf_persistently {p : Bool} [BI PROP] {P : PROP} :
    <pers>?p <pers> P ⊣⊢ <pers> P

theorem false_elim [BI PROP] {P : PROP} : False ⊢ P

theorem equiv_of_some_equiv_some {x y : α} (H : some x ≡ some y) : x ≡ y

theorem id [BI PROP] : ⊢ (∃ x, x : PROP)

theorem move_multiple [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q

theorem Heap.get_point [Heap T K V] {k k' : K} {v : Option V} :
    get (point k v : T) k' = if k = k' then v else .none

@[elab_as_elim]
theorem OFE.ContractiveHom.fixpoint_ind [COFE α] [Inhabited α] (f : α -c> α)
    (P : α → Prop) (HProper : ∀ A B : α, A ≡ B → P A → P B) (x : α) (Hbase : P x)
    (Hind : ∀ x, P x → P (f x)) (Hlim : LimitPreserving P) :
    P f.fixpoint

theorem persistently_sep [BI PROP] [BIPositive PROP] {P Q : PROP} :
    <pers> (P ∗ Q) ⊣⊢ <pers> P ∗ <pers> Q

theorem LocalUpdate.unit {x y x' y' : Unit} : (x, y) ~l~> (x', y')

theorem persistently_true [BI PROP] : <pers> (True : PROP) ⊣⊢ True

theorem imp_wand_1 [BI PROP] [BIAffine PROP] {P Q : PROP} : (P → Q) ⊢ P -∗ Q

theorem bupd_frame_l {P Q : PROP} : iprop(P ∗ |==> Q ⊢ |==> (P ∗ Q))

theorem LocalUpdate.option {x y x' y' : α}
    (h : (x, y) ~l~> (x', y')) : (some x, some y) ~l~> (some x', some y')

theorem apply_forall_intuitionistic' [BI PROP] (P Q : α → PROP) (a b : α) : (□ ∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b

theorem sep_mono_r [BI PROP] {P Q Q' : PROP} (h : Q ⊢ Q') : P ∗ Q ⊢ P ∗ Q'

theorem or_symm [BI PROP] {P Q : PROP} : P ∨ Q ⊢ Q ∨ P

theorem exists_intuitionistic [BI PROP] (Q : Nat → PROP) : □ (∃ x, Q x) ⊢ ∃ x, □ Q x ∨ False

theorem hmap_alloc [Heap T K V] {t : T} (H : get t k = some v) : get (hmap f t) k = f k v

theorem not_add_lt_self {a b : α} : ¬a + b < a

theorem UpdateP.trans {x : α} (ux : x ~~>: P) (upq : ∀ y, P y → y ~~>: Q) : x ~~>: Q

theorem Agree.valid_included {x y : Agree α} : ✓ y → x ≼ y → x ≡ y

theorem absorbinglyIf_sep_r {p : Bool} [BI PROP] {P Q : PROP} :
    P ∗ <absorb>?p Q ⊣⊢ <absorb>?p (P ∗ Q)

theorem apply_forall' [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b

theorem intuitionistically_affinely [BI PROP] {P : PROP} : □ <affine> P ⊣⊢ □ P

theorem absorbingly_sep_l [BI PROP] {P Q : PROP} : <absorb> P ∗ Q ⊣⊢ <absorb> (P ∗ Q)

theorem pure_sep [BI PROP] {φ1 φ2 : Prop} : ⌜φ1⌝ ∗ (⌜φ2⌝ : PROP) ⊣⊢ ⌜φ1 ∧ φ2⌝

theorem inc_iff_incN [OFE.Discrete α] (n) {x y : α} : x ≼ y ↔ x ≼{n} y

@[simp] theorem Iso.inv_hom_dist [OFE α] [OFE β] (iso : Iso α β) {n} {x} :
    iso.inv (iso.hom x) ≡{n}≡ x

theorem pure_congr [BI PROP] {φ1 φ2 : Prop} (h : φ1 ↔ φ2) : ⌜φ1⌝ ⊣⊢ (⌜φ2⌝ : PROP)

theorem down_eqToHom {k k'} {x : A F (k+1)} (e : k = k') :
    down F k' (eqToHom (congrArg Nat.succ e) x) = eqToHom e (down F k x)

theorem later_exists_2 [BI PROP] {Φ : α → PROP} :
    (∃ a, ▷ Φ a) ⊢ ▷ (∃ a, Φ a)

theorem incN_trans {x y z : α} : x ≼{n} y → y ≼{n} z → x ≼{n} z

theorem pcore_eq_core (x : α) : pcore x = some (core x)

theorem sep_right [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -∗ P ∗ Q

theorem persistently_absorb_r [BI PROP] {P Q : PROP} : P ∗ <pers> Q ⊢ <pers> Q

theorem IdFree.of_eqv {x₁ x₂ : α} (e : x₁ ≡ x₂) (h : IdFree x₁) : IdFree x₂

theorem persistently_and_iff_sep [BI PROP] [BIAffine PROP] {P Q : PROP} :
    <pers> P ∧ Q ⊣⊢ <pers> P ∗ Q

theorem persistently_emp [BI PROP] : <pers> (emp : PROP) ⊣⊢ True

theorem validN_of_eqv {x y : α} : x ≡ y → ✓{n} x → ✓{n} y

theorem pure_wand [BI PROP] {φ1 φ2 : Prop} : (⌜φ1⌝ -∗ (⌜φ2⌝ : PROP)) ⊣⊢ ⌜φ1 → φ2⌝

theorem _root_.Iris.OFE.Dist.op {x x' y y' : α}
    (ex : x ≡{n}≡ x') (ey : y ≡{n}≡ y') : x • y ≡{n}≡ x' • y'

theorem and_destruct_intuitionistic_right [BI PROP] (Q : PROP) : □ (P ∧ Q) ⊢ Q

theorem biaffine_iff_true_emp [BI PROP] : BIAffine PROP ↔ (True : PROP) ⊢ emp

theorem persistently_and_emp {P : PROP} [BI PROP] : <pers> P ⊣⊢ <pers> (emp ∧ P)

theorem plainly_forall_2 {Ψ : α → PROP} : (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a)

theorem op_some_opM_assoc_dist {x y : α} {mz : Option α} : (x • y) •? mz ≡{n}≡ x •? (some y • mz)

theorem absorbinglyIf_forall_1 {p : Bool} [BI PROP] {Φ : α → PROP} :
    <absorb>?p (∀ a, Φ a) ⊢ ∀ a, <absorb>?p (Φ a)

theorem sep_or_r [BI PROP] {P Q R : PROP} : (P ∨ Q) ∗ R ⊣⊢ (P ∗ R) ∨ (Q ∗ R)

@[simp] theorem affinelyIf_false [BI PROP] (P : PROP) : iprop(<affine>?false P) = P

theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
    (h1 : P ⊢ A2) : P ⊢ Q

theorem plainly_wand_affinely_plainly : (<affine> ■ P -∗ ■ Q) ⊢ ■ (<affine> ■ P -∗ Q)

theorem incN_of_dist_of_incN (e : (a : α) ≡{n}≡ b) : b ≼{n} c → a ≼{n} c

theorem LocalUpdate.id (x : α × α) : x ~l~> x

@[rw_mono_rule]
theorem wandIff_congr [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊣⊢ Q) (h2 : P' ⊣⊢ Q') :
    (P ∗-∗ P') ⊣⊢ (Q ∗-∗ Q')

theorem Agree.op_ne₂ : OFE.NonExpansive₂ (Agree.op (α := α))

theorem incN_iff_isTotal [IsTotal α] {ma mb : Option α} :
    ma ≼{n} mb ↔ ma = none ∨ ∃ a b, ma = some a ∧ mb = some b ∧ a ≼{n} b

theorem id_free_r {x : α} [IdFree x] {y} (v : ✓x) : ¬(x • y ≡ x)

theorem Agree.valid_def {x : Agree α} : ✓ x ↔ x.valid

theorem emp_and [BI PROP] {P : PROP} [Affine P] : emp ∧ P ⊣⊢ P

theorem bupd_plain_forall {A : Type} (Φ : A → PROP) [∀ x, Plain (Φ x)] :
    (|==> ∀ x, Φ x) ⊣⊢ (∀ x, |==> Φ x)

theorem exact_lean [BI PROP] (Q : PROP) (H : ⊢ Q) : ⊢ Q

theorem sep_congr_l [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : P ∗ Q ⊣⊢ P' ∗ Q

theorem UpdateP.iso
    (gf : ∀ x, g (f x) ≡ x)
    (g_op : ∀ y1 y2, g (y1 • y2) ≡ g y1 • g y2)
    (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y)
    (uyp : y ~~>: P)
    (pq : ∀ y', P y' → Q (g y')) :
    g y ~~>: Q

theorem sep_emp [BI PROP] {P : PROP} : P ∗ emp ⊣⊢ P

theorem pure_soundness : iprop(True ⊢ (⌜P⌝ : UPred M)) → P

theorem Eq_Equivalence {α : Type _} : Equivalence (@Eq α)

theorem discrete_id_free {x : α} [Discrete α] (H : ∀ y, ✓ x → ¬(x • y ≡ x)) : IdFree x

@[rw_mono_rule]
theorem persistently_congr [BI PROP] {P P' : PROP} (h : P ⊣⊢ P') :
    <pers> P ⊣⊢ <pers> P'

theorem absorbingly_elim_plainly : <absorb> ■ P ⊣⊢ ■ P

theorem affine_affinely [BI PROP] (P : PROP) [Affine P] : <affine> P ⊣⊢ P

theorem wand_elim_l [BI PROP] {P Q : PROP} : (P -∗ Q) ∗ P ⊢ Q
</all_available_lemmas>

<local_ctx>
import Iris.BI.Classes

import Iris.BI.Extensions

import Iris.BI.BI

import Iris.Std.Classes

import Iris.Std.Rewrite

import Iris.Std.TC

namespace Iris.BI

open Iris.Std BI
</local_ctx>

<target_theorem>
theorem later_exists_false [BI PROP] {Φ : α → PROP} :
    (▷ ∃ a, Φ a) ⊢ ▷ False ∨ ∃ a, ▷ Φ a :=
</target_theorem>

