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>
class Reflexive (R : Relation α) where
  refl {x : α} : R x x

class Commutative (R : Relation α) (f : β → β → α) where
  comm {x y : β} : R (f x y) (f y x)

class Associative (R : Relation α) (f : α → α → α) where
  assoc {x y z : α} : R (f (f x y) z) (f x (f y z))

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₂

class Discrete (α : Type _) [OFE α] where
  discrete_0 {x y : α} : x ≡{0}≡ y → 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 -/

@[ext] structure Iso (α β : Type _) [OFE α] [OFE β] where
  hom : α -n> β
  inv : β -n> α
  hom_inv : hom (inv x) ≡ x
  inv_hom : inv (hom x) ≡ x

def Iso.symm [OFE α] [OFE β] (iso : Iso α β) : Iso β α where
  hom := iso.inv
  inv := iso.hom
  hom_inv := by admit /- proof elided -/

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

inductive DFrac (F : Type _) where
 
| own (f : F) : DFrac F
 
| discard : DFrac F
 
| ownDiscard (f : F) : DFrac F

def pcore : DFrac F → Option (DFrac F)
  | own _        => none
  | .discard     => some discard
  | ownDiscard _ => some discard

def op : DFrac F → DFrac F → DFrac F
  | .discard, .discard => discard
  | own f, .discard
  | ownDiscard f, .discard
  | .discard, own f
  | .discard, ownDiscard f => ownDiscard f
  | own f, own f' => own (f + f')
  | own f, ownDiscard f'
  | ownDiscard f, own f'
  | ownDiscard f, ownDiscard f' => ownDiscard (f + f')

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

op_ne : NonExpansive (op x)
  pcore_ne : x ≡{n}≡ y → pcore x = some cx →
    ∃ cy, pcore y = some cy ∧ cx ≡{n}≡ cy
  validN_ne : x ≡{n}≡ y → ValidN n x → ValidN n y

valid_iff_validN : Valid x ↔ ∀ n, ValidN n x
  validN_succ : ValidN n.succ x → ValidN n x
  validN_op_left : ValidN n (op x y) → ValidN n x

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

pcore_op_left : pcore x = some cx → op cx x ≡ x
  pcore_idem : pcore x = some cx → pcore cx ≡ some cx
  pcore_op_mono : pcore x = some cx → ∀ y, ∃ cy, pcore (op x y) ≡ some (op cx cy)

extend : ValidN n x → x ≡{n}≡ op y₁ y₂ →
    Σ' z₁ z₂, x ≡ op z₁ z₂ ∧ z₁ ≡{n}≡ y₁ ∧ z₂ ≡{n}≡ y₂

def Included (x y : α) : Prop := ∃ z, y ≡ x • z

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

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

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

instance intoSep_persistently_affine [BI PROP] (P Q1 Q2 : PROP) [h : IntoSep P Q1 Q2]
    [TCOr (Affine Q1) (Absorbing Q2)] [TCOr (Affine Q2) (Absorbing Q1)] :
    IntoSep iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2) where
  into_sep := (persistently_mono <| h.1.trans sep_and).trans <|
    persistently_and.1.trans persistently_and_imp_sep

ULift.down in Init.Prelude

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

class FromAffinely [BI PROP] (P : outParam PROP) (Q : PROP) (p : Bool := true) where
  from_affinely : <affine>?p Q ⊢ P

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

Lean.MacroM in Init.Prelude

partial def SpecPat.parse (pat : Syntax) : MacroM SpecPat := do
  match go ⟨← expandMacros pat⟩ with
  | none => Macro.throwUnsupported
  | some pat => return pat
where
  go : TSyntax `specPat → Option SpecPat
  | `(specPat| $name:binderIdent) => some <| .ident name
  | `(specPat| [$[$names:binderIdent],*]) => some <| .idents names.toList .anonymous
  | `(specPat| [$[$names:binderIdent],*] as $goal:ident) => match goal.raw with
    | .ident _ _ val _ => some <| .idents names.toList val
    | _ => none
  | _ => none

instance fromPure_pure_or (a1 a2 : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
    [h1 : FromPure a1 P1 φ1] [h2 : FromPure a2 P2 φ2] :
    FromPure (a1 || a2) iprop(P1 ∨ P2) (φ1 ∨ φ2) where
  from_pure := (affinelyIf_mono pure_or.2).trans <| affinelyIf_or.1.trans <| by
    refine or_mono ((affinelyIf_flag_mono ?_).trans h1.1) ((affinelyIf_flag_mono ?_).trans h2.1)
      <;> simp_all

instance {f : F} : CMRA.Cancelable (own f) where
  cancelableN {_} := by admit /- proof elided -/

@[simp] def optionCore (x : Option α) : Option α := x.bind pcore

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 fromOr_persistently [BI PROP] (P Q1 Q2 : PROP) [h : FromOr P Q1 Q2] :
    FromOr iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2) where
  from_or := persistently_or.2.trans (persistently_mono h.1)

instance [OFE α] [OFE β] : OFE (α -c> β) where
  Equiv f g := Equiv f.toHom g.toHom
  Dist n f g := Dist n f.toHom g.toHom
  dist_eqv := {
    refl _ := dist_eqv.refl _
    symm h := dist_eqv.symm h
    trans h1 h2 := dist_eqv.trans h1 h2
  }
  equiv_dist := equiv_dist
  dist_lt := dist_lt

let state ← saveState
    if let some goals ← applyMonotonicity goal then
      let mut rule? := some rule

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

Lean.Expr in Lean.Expr

instance : OFE (Agree α) where
  Equiv x y := ∀ n, Agree.dist n x y
  Dist := Agree.dist
  dist_eqv := Agree.dist_equiv
  equiv_dist := by admit /- proof elided -/

Add.add in Init.Prelude

class Heap (T : Type _) (K V : outParam (Type _)) extends Store T K (Option V) where
  empty : T
  hmap (f : K → V → Option V) : T → T
  merge (op : V → V → V) : T → T → T
  get_empty : get empty k = none
  get_hmap : get (hmap f t) k = (get t k).bind (f k)
  get_merge : get (merge op t1 t2) k = Option.merge op (get t1 k) (get t2 k)

Unit in Init.Prelude

Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg in Lean.PrettyPrinter.Delaborator.SubExpr

instance (y : α) : CoreId (core y) := CoreId.of_pcore_eq_some (pcore_eq_core _)

instance intuitionisticallyIf_affine (p : Bool) [BI PROP] (P : PROP) [Affine P] :
    Affine iprop(□?p P) :=

instance : Trans (IncludedN (α := α) n) (IncludedN n) (IncludedN n) where
  trans := incN_trans

def toAgree (a : α) : Agree α := ⟨[a], by admit /- proof elided -/
⟩

instance [BI PROP] [BIAffine PROP] : LeftId (α := PROP) BiEntails iprop(True) sep := ⟨true_sep⟩

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)

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

Lean.PrettyPrinter.Delaborator.SubExpr.getExpr in Lean.PrettyPrinter.Delaborator.SubExpr

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

def cmraValid [CMRA A] (a : A) : UPred M where
  holds n _ := ✓{n} a
  mono hv _ le := CMRA.validN_of_le le hv

instance [BI PROP] [BIAffine PROP] : RightId (α := PROP) BiEntails emp and := ⟨and_emp⟩

let (_, hyps) ← delabHypotheses hyps ({}, #[])
  let goal ← unpackIprop (← delab goal)

Qq.instantiateMVarsQ in Qq.MetaM

| .conjunction [] => iCasesEmptyConj bi hyps Q A' p @k

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

instance fromPure_absorbingly (a : Bool) [BI PROP] (P : PROP) (φ : Prop)
    [h : FromPure a P φ] : FromPure false iprop(<absorb> P) φ where
  from_pure := absorbingly_affinely_intro_of_persistent.trans <|
    absorbingly_mono <| affinely_affinelyIf.trans h.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)

instance intoPure_pure_or (φ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 := (or_mono h1.1 h2.1).trans pure_or.1

instance NextContractive {A : Type} [OFE A] : Contractive (@Later.next A) where
  distLater_dist := id

protected def Hom.id [OFE α] : α -n> α where
  f := id
  ne.ne _ _ _ := id

instance : Trans (Included (α := α)) Included Included where
  trans := inc_trans

inductive splitSide where
| splitLeft | splitRight

protected def imp (P Q : UPred M) : UPred M where
  holds n x := ∀ n' x', x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x'
  mono {n₁ n₂ x₁ x₂} H := fun ⟨m₁, Hle⟩ Hn n x ⟨m₂, Hxle⟩ Hnle Hv HP => by admit /- proof elided -/

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 intoPure_pure_and (φ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 := (and_mono h1.1 h2.1).trans pure_and.1

class Antisymmetric (R : Relation α) (S : outParam <| Relation α) where
  antisymm {x y : α} : (left : S x y) → (right : S y x) → R x y

def clearCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' out goal : Q($prop))
    (pf : Q($e ⊣⊢ $e' ∗ $out)) : MetaM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do
  if out.isAppOfArity ``intuitionistically 3 then
    have out' : Q($prop) := out.appArg!
    have : $out =Q iprop(□ $out') := ⟨⟩
    pure q(clear_intuitionistic (Q := $goal) $pf)
  else
    let _ ← synthInstanceQ q(TCOr (Affine $out) (Absorbing $goal))
    pure q(clear_spatial $pf)

instance : BUpd (UPred M) := ⟨bupd⟩

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

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

Option.map in Init.Prelude

def Agree.dist (n : Nat) (x y : Agree α) : Prop :=
  (∀ a ∈ x.car, ∃ b ∈ y.car, a ≡{n}≡ b) ∧
  (∀ b ∈ y.car, ∃ a ∈ x.car, a ≡{n}≡ b)

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

def getFreshName : TSyntax ``binderIdent → CoreM (Name × Syntax)
  | `(binderIdent| $name:ident) => pure (name.getId, name)
  | stx => return (← mkFreshUserName `x, stx)

def binderIdentHasName (name : Name) (id : TSyntax ``binderIdent) : Bool :=
  match id with
  | `(binderIdent| $name':ident) => name'.getId == name
  | _ => false

inductive StateResult (α : Type _)
  | unknown
  | result (x : α)
  | conflict

instance [URFunctorContractive F] : COFE.OFunctorContractive (UPredOF F) where
  map_contractive.1 {_ x y} HKL _ _ _ Hn _ := by admit /- proof elided -/

instance : CoeFun (Tower F) (fun _ => ∀ k, A F k) := ⟨Tower.val⟩

instance and_absorbing [BI PROP] (P Q : PROP) [Absorbing P] [Absorbing Q] :
    Absorbing iprop(P ∧ Q) where
  absorbing := absorbingly_and_1.trans (and_mono absorbing absorbing)

instance : UFraction α where
  Proper x := x ≤ 1
  add_comm := add_comm
  add_assoc := add_assoc
  add_left_cancel := add_left_cancel
  add_ne H := add_ne_self ((add_comm ..).trans H.symm)
  proper_add_mono_left := add_le_mono
  
  
  
  
  
  
  
  one_whole := by admit /- proof elided -/

id in Init.Prelude

instance : OFE.NonExpansive (ownM : M → UPred M) where
  ne _ _ _ H _ _ Hn _ := OFE.Dist.incN (OFE.Dist.le H Hn) .rfl

instance isOFE_later [OFE A] : OFE (Later A) where
  Equiv x y := x.car ≡ y.car
  Dist n x y := DistLater n x.car y.car
  dist_eqv := ⟨fun _ => .rfl, .symm, .trans⟩
  equiv_dist := by admit /- proof elided -/

def iPrePropO : Type _ := OFunctor.Fix (UPredOF (IResF FF))

def IrisGoal.toExpr : IrisGoal → Expr
  | { hyps, goal, .. } => q(Entails' $(hyps.tm) $goal)

instance fromWand_wand [BI PROP] (P1 P2 : PROP) : FromWand iprop(P1 -∗ P2) P1 P2 := ⟨.rfl⟩

Lean.Elab.throwUnsupportedSyntax in Lean.Elab.Exception

class RepFunStore (T : Type _) (K V : outParam (Type _)) [Store T K V] where
  rep : (K → V) → Prop
  rep_get (t : T) : rep (get t)
  of_fun : { f : K → V // rep f } → T
  get_of_fun : get (of_fun f) = f

Or in Init.Prelude

instance : COFE (Fix F) := inferInstanceAs (COFE (Tower F))

instance [Fraction α] [CMRA α] {a : Frac α} (Hw : Whole a.1) : Exclusive a where
  exclusive0_l _ Hk := (not_exists.mp Hw.2) _ Hk

instance : TCTrue := TCTrue.t

instance [BI PROP] : Associative (α := PROP) BiEntails sep := ⟨sep_assoc⟩

instance : BIPlainly (UPred M) where
  mono H _ _ _ := H _ _ CMRA.unit_validN
  elim_persistently {P} n x Hx := by admit /- proof elided -/

applyReflexivity (goal : MVarId) : TacticM Unit := do
    try
      discard <| apply' goal ``refl
    catch _ => pure ()

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

def matchBool (p : Q(Bool)) : ($p =Q true) ⊕' ($p =Q false) :=
  if isTrue p then .inl ⟨⟩ else .inr ⟨⟩

instance fromPure_pure [BI PROP] (φ : Prop) : FromPure (PROP := PROP) false iprop(⌜φ⌝) φ := ⟨.rfl⟩

instance intoWand_intuitionistically (p q : Bool) [BI PROP] (R P Q : PROP)
    [h : IntoWand true q R P Q] : IntoWand p q iprop(□ R) P Q where
  into_wand := (intuitionisticallyIf_mono h.1).trans intuitionisticallyIf_elim

instance asEmpValid1_entails [BI PROP] (P Q : PROP) : AsEmpValid1 (P ⊢ Q) iprop(P -∗ Q) where
  as_emp_valid := ⟨entails_wand, wand_entails⟩

Lean.Elab.Tactic.getUnsolvedGoals in Lean.Elab.Tactic.Basic

instance (priority := default - 10) asEmpValidEmpValid1
    [BI PROP] (P : PROP) : AsEmpValid1 (⊢ P) P := ⟨by admit /- proof elided -/
    ⟩

abbrev IProp := UPred (IResUR FF)

def setMDataName? (e : Expr) (name : Name) : Expr := match e with
  | Expr.mdata md e =>
    mkMData (md.insert `name name) e
  | e =>
    mkMData (KVMap.empty.insert `name name) e

instance (priority := default + 10) fromSep_affinely [BI PROP] (P Q1 Q2 : PROP)
    [h : FromSep P Q1 Q2] : FromSep iprop(<affine> P) iprop(<affine> Q1) iprop(<affine> Q2) where
  from_sep := affinely_sep_2.trans (affinely_mono h.1)

instance (priority := default - 10) intoAbsorbingly_default [BI PROP] (P : PROP) :
    IntoAbsorbingly iprop(<absorb> P) P := ⟨.rfl⟩

instance intoSep_and_persistent_l [BI PROP] (P Q P' Q' : PROP) [Persistent P]
    [inst : AndIntoSep P P' Q Q'] : IntoSep iprop(P ∧ Q) P' Q' where
  into_sep :=
    match P', inst with
    | _, AndIntoSep.affine (h := h) .. =>
      (and_mono_l (affine_affinely _).2).trans <| affinely_and_lr.1.trans <|
        persistent_and_affinely_sep_l_1.trans (sep_mono (affine_affinely _).1 h.1)
    | _, AndIntoSep.affinely .. => persistent_and_affinely_sep_l_1

def Iso.comp [OFE α] [OFE β] [OFE γ] (iso1 : Iso β γ) (iso2 : Iso α β) : Iso α γ where
  hom := iso1.hom.comp iso2.hom
  inv := iso2.inv.comp iso1.inv
  hom_inv := by admit /- proof elided -/

instance fromAssumption_later [BI PROP] (p : Bool) (P Q : PROP)
    [h : FromAssumption p P Q] : FromAssumption p P iprop(▷ Q) where
  from_assumption := h.1.trans later_intro

def Agree.map' {α β} (f : α → β) (a : Agree α) : Agree β := ⟨a.car.map f, by admit /- proof elided -/
⟩

@[delab app.Iris.ProofMode.HypMarker]
def delabHypMarker : Delab := do unpackIprop (← withAppArg delab)

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

instance : OFE.NonExpansive (@toAgree α) where
  ne n x₁ x₂ heq := by admit /- proof elided -/

def Disjoint {X : Type _} (S1 S2 : X → Prop) : Prop :=
  ∀ x : X, ¬(S1 x ∧ S2 x)

instance (priority := default + 30) intoAbsorbingly_true [BI PROP] :
    IntoAbsorbingly (PROP := PROP) iprop(True) emp where
  into_absorbingly := absorbingly_emp.2

instance discrete_op {x y : α} (Hv : ✓{0} x • y) [Hx : DiscreteE x] [Hy : DiscreteE y] :
    DiscreteE (x • y) where
  discrete h :=
    let ⟨_w, _t, wt, wx, ty⟩ := extend ((Dist.validN h).mp Hv) h.symm
    ((Hx.discrete wx.symm).op (Hy.discrete ty.symm)).trans wt.symm

class OFE (α : Type _) where
  Equiv : α → α → Prop
  Dist : Nat → α → α → Prop
  dist_eqv : Equivalence (Dist n)
  equiv_dist : Equiv x y ↔ ∀ n, Dist n x y
  dist_lt : Dist n x y → m < n → Dist m x y

instance intoPure_pure (φ : Prop) [BI PROP] : IntoPure (PROP := PROP) iprop(⌜φ⌝) φ := ⟨.rfl⟩

abbrev LaterOF (F : OFunctorPre) : OFunctorPre :=
  fun A B _ _ => Later (F A B)

protected def pure (p : Prop) : UPred M where
  holds _ _ := p
  mono h _ _ := h

instance (priority := default + 20) fromSep_pure (φ ψ : Prop) [BI PROP] :
    FromSep (PROP := PROP) iprop(⌜φ ∧ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝) where
  from_sep := pure_sep.1

@[simp] def optionValidN (n : Nat) : Option α → Prop
  | some x => ✓{n} x
  | none => True

@[simp] def optionOp (x y : Option α) : Option α :=
  match x, y with
  | some x', some y' => some (CMRA.op x' y')
  | none, _ => y
  | _, none => x

instance absorbingly_absorbing [BI PROP] (P : PROP) : Absorbing iprop(<absorb> P) where
  absorbing := absorbingly_idem.1

instance oFunctorLater [OFunctor F] : OFunctor (LaterOF F) where
  cofe := _
  map f g := laterMap (OFunctor.map f g)
  map_ne.ne _ _ _ Hx _ _ Hy _ _ := (OFunctor.map_ne.ne Hx Hy _).lt
  map_id _ := OFunctor.map_id _
  map_comp _ _ _ _ _ := OFunctor.map_comp ..

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

instance sep_absorbing_r [BI PROP] (P Q : PROP) [Absorbing Q] : Absorbing iprop(P ∗ Q) where
  absorbing := absorbingly_sep_r.2.trans (sep_mono_r absorbing)

instance intoAnd_sep_affine (p : Bool) [BI PROP] (P Q : PROP)
    [TCOr (Affine P) (Absorbing Q)] [TCOr (Affine Q) (Absorbing P)] :
    IntoAnd p iprop(P ∗ Q) P Q where
  into_and := intuitionisticallyIf_mono sep_and

def GName := LeibnizO Nat

Lean.Syntax.TSepArray in Init.Prelude

def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e)
  | _, .emp _ => none
  | _, .sep _ _ _ _ lhs rhs =>
    match rhs.rename with
    | some rhs' => some (.mkSep lhs rhs' _)
    | none => match lhs.rename with
      | some lhs' => some (.mkSep lhs' rhs _)
      | none => none
  | _, .hyp _ _ uniq p ty _ =>
    if oldUniq == uniq then some (Hyps.mkHyp bi new uniq p ty _) else none

def Set (α : Type _) := α → Prop

Lean.Parser.Tactic.rwRule in Init.Tactics

instance fromExists_persistently [BI PROP] (P : PROP) (Φ : α → PROP) [h : FromExists P Φ] :
    FromExists iprop(<pers> P) (fun a => iprop(<pers> (Φ a))) where
  from_exists := persistently_exists.2.trans <| persistently_mono h.1

instance sep_persistent [BI PROP] (P Q : PROP) [Persistent P] [Persistent Q] :
    Persistent iprop(P ∗ Q) where
  persistent := (sep_mono persistent persistent).trans persistently_sep_2

instance (priority := default + 20) intoAbsorbingly_absorbing [BI PROP] (P : PROP) [Absorbing P] :
    IntoAbsorbingly P P where
  into_absorbingly := absorbing_absorbingly.2

instance (priority := default + 10) intoPersistently_self [BI PROP] (P : PROP) :
    IntoPersistently true P P := ⟨.rfl⟩

instance : OFE.NonExpansive (plainly : UPred M → UPred M) where
  ne n P1 P2 HP n' y Hn' Hy := by admit /- proof elided -/

Inhabited in Init.Prelude

Lean.mkFreshId in Init.Meta.Defs

instance unit_total : IsTotal α where
  total _ :=
    have ⟨y, hy, _⟩ := pcore_mono' inc_unit pcore_unit
    ⟨y, hy⟩

instance : IsModal (PROP1 := PROP) affinely (.id rfl) (.forall rfl Affine) where
  spec_intuitionistic _ := affinely_intro .rfl
  spec_spatial _ _ := affinely_intro .rfl
  emp := affinely_intro .rfl
  mono := (affinely_mono ·)
  sep := affinely_sep_2

| .conjunction [arg] | .disjunction [arg] => iCasesCore hyps Q p A A' ⟨⟩ arg @k

instance {P : PROP} [Plain P] : Plain iprop(|==> P) :=
  ⟨(mono Plain.plain).trans <| (bupd_elim).trans <| BIPlainly.mono intro⟩

def headName (spats : List SpecPat) : Name :=
  match spats.head? with
    | some <| .ident _ => .anonymous
    | some <| .idents _ name => name
    | _ => .anonymous

instance [CMRA α] : Trans Update OFE.Equiv Update (α := α) where
  trans u e := Update.equiv_right e u

go (goal : MVarId) (rule : TSyntax `term) : TacticM Bool := do
    
    try
      withFocus goal <| withoutRecover <| evalTactic (← `(tactic|
        exact $rule
      ))
      return true
    catch _ => pure ()

class AsEmpValid2 (φ : Prop) {PROP : outParam (Type _)} (P : outParam PROP) [BI PROP] where
  as_emp_valid : φ ↔ ⊢ P

instance [BI PROP] [BIAffine PROP] : RightId (α := PROP) BiEntails iprop(True) sep := ⟨sep_true⟩

def up : ∀ k, A F k -n> A F (k+1)
  | 0 => ⟨fun _ => inh.default, ⟨fun _ _ _ _ => .rfl⟩⟩
  | k+1 => map (down k) (up k)

Inhabited.default in Init.Prelude
</all_available_defs>

<all_available_lemmas>
@[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 Equiv.dist [OFE α] {x : α} : x ≡ y → x ≡{n}≡ y

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

theorem op_right_eqv (x : α) {y z : α} (e : y ≡ z) : x • y ≡ x • z

theorem _root_.Iris.OFE.Equiv.op_r {x y z : α} : y ≡ z → x • y ≡ x • z

theorem op_right_dist (x : α) {y z : α} (e : y ≡{n}≡ z) : x • y ≡{n}≡ x • z

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

theorem op_left_eqv {x y : α} (z : α) (e : x ≡ y) : x • z ≡ y • z

theorem op_left_dist {x y : α} (z : α) (e : x ≡{n}≡ y) : x • z ≡{n}≡ y • z

theorem Valid.validN : ✓ (x : α) → ✓{n} x

theorem validN_iff {x y : α} (e : x ≡{n}≡ y) : ✓{n} x ↔ ✓{n} y

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

theorem validN_of_le {n n'} {x : α} : n' ≤ n → ✓{n} x → ✓{n'} x

theorem inc_trans {x y z : α} : x ≼ y → y ≼ z → x ≼ z

theorem Included.trans : (x : α) ≼ y → y ≼ z → x ≼ z

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

theorem IncludedN.trans : (x : α) ≼{n} y → y ≼{n} z → x ≼{n} z

theorem validN_of_incN {n} {x y : α} : x ≼{n} y → ✓{n} y → ✓{n} x

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

theorem validN_of_inc {n} {x y : α} : x ≼ y → ✓{n} y → ✓{n} x

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

theorem valid_iff_validN' [Discrete α] (n) {x : α} : ✓ x ↔ ✓{n} x

theorem unit_left_id_dist {n} (x : α) : unit • x ≡{n}≡ x

theorem unit_right_id_dist (x : α) : x • unit ≡{n}≡ x

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

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

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

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

@[rw_mono_rule]
theorem and_congr [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊣⊢ Q) (h2 : P' ⊣⊢ Q') : P ∧ P' ⊣⊢ Q ∧ Q'

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

theorem or_true [BI PROP] {P : PROP} : P ∨ True ⊣⊢ True

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

theorem lookup_inc {m1 m2 : T} :
    (∃ (z : T), m2 ≡ op m1 z) ↔
    ∀ i, (∃ z, (get m2 i) ≡ (get m1 i) • z)

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

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

theorem from_affine [BI PROP] {p : Bool} {P P' Q : PROP} [hP : FromAffinely P' P p] :
    Replaces Q iprop(□?p P) P'

theorem later_or [BI PROP] {P Q : PROP} : ▷ (P ∨ Q) ⊣⊢ ▷ P ∨ ▷ Q

theorem bigOp_sep_nil [BI PROP] : iprop([∗] []) ⊣⊢ (emp : PROP)

theorem valid_0_iff_validN [Discrete α] (n) {x : α} : ✓{0} x ↔ ✓{n} x

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

@[simp]
theorem Agree.toAgree_included {a b : α} : toAgree a ≼ toAgree b ↔ a ≡ b

theorem Update.total [CMRA.IsTotal α] :
    x ~~> y ↔ ∀ (n : Nat) (z : α), ✓{n} (x • z) → ✓{n} (y • z)

@[simp]
theorem Agree.toAgree_included_L [OFE.Leibniz α] {a b : α} :
    toAgree a ≼ toAgree b ↔ a = b

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

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

theorem Tower.embed_self (X : Tower F) :
    Tower.embed (k+1) (X (k+1)) ≡{k}≡ X

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

theorem false_imp [BI PROP] {P : PROP} : (False → P) ⊣⊢ True

theorem later_forall [BI PROP] {Φ : α → PROP} :
    ▷ (∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a)

theorem pure_mono [BI PROP] {φ1 φ2 : Prop} (h : φ1 → φ2) : ⌜φ1⌝ ⊢ (⌜φ2⌝ : PROP)

theorem absorbingly_intro [BI PROP] {P : PROP} : P ⊢ <absorb> P

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

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

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

theorem to_persistent_spatial [BI PROP] {P P' Q : PROP}
    [hP : IntoPersistently false P P'] [or : TCOr (Affine P) (Absorbing Q)] :
    Replaces Q P iprop(□ P')

theorem _root_.Iris.OFE.Dist.incN :
    (a : α) ≡{n}≡ a' → b ≡{n}≡ b' → (a ≼{n} b ↔ a' ≼{n} b')

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

theorem affinely_plainly_elim : <affine> ■ P ⊢ P

theorem valid_disjoint_dom {m1 m2 : T} (Hv : ✓ (m1 • m2)) (H : ∀ {k x}, get m1 k = some x → Exclusive x) :
    Set.Disjoint (dom m1) (dom m2)

theorem empty_union {s : State Val} : s = ∅ ∪ s

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

theorem affine_env [BI PROP] (P : PROP) : <affine> P ⊢ emp

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

theorem false_intro [BI PROP] (Q : PROP) : False ⊢ Q

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

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

theorem or_exists_bool [BI PROP] {P Q : PROP} :
    P ∨ Q ⊣⊢ «exists» (fun b : Bool => if b then P else Q)

theorem later_congr [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : ▷ P ⊣⊢ ▷ Q

theorem intuitionistically_plainly : □ ■ P ⊢ ■ □ P

theorem core_id_dup_L {x : α} [CoreId x] : x • x = x

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

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

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

theorem ownM_valid (m : M) : ownM m ⊢ cmraValid m

theorem exists_intro' [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists Q Φ]
    (a : α) (h : P ⊢ Φ a) : P ⊢ Q

theorem impl_wand_affinely_plainly : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ Q)

theorem eqv_of_inc_exclusive [Exclusive (a : α)] {b : α} (H : some a ≼ some b) (Hv : ✓ b) :
     a ≡ b

theorem disjunction_clear [BI PROP] [BIAffine PROP] (Q : PROP) : Q ⊢ P1 ∨ P2 -∗ Q

theorem intuitionistically_sep [BI PROP] [BIPositive PROP] {P Q : PROP} : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q

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

theorem persistently_and_affinely_sep [BI PROP] {P Q : PROP} : <pers> P ∧ Q ⊢ <affine> P ∗ Q

theorem Store.get_set [Store T K V] {t : T} {k k' : K} {v : V} :
    get (set t k v) k' = if k = k' then v else get t k'

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

theorem intuitionisticallyIf_and {p : Bool} [BI PROP] {P Q : PROP} : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q

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

theorem as_emp_valid_2 [BI PROP] (φ : Prop) [AsEmpValid2 φ (P : PROP)] : (⊢ P) → φ

theorem HγE  (i : GId FF1) : i = γ

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

theorem _root_.Iris.OFE.Dist.opM {x₁ x₂ : α} {y₁ y₂ : Option α}
    (H1 : x₁ ≡{n}≡ x₂) (H2 : y₁ ≡{n}≡ y₂) : x₁ •? y₁ ≡{n}≡ x₂ •? y₂

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

theorem not_valid_some_exclN_op_left {n} {x : α} [Exclusive x] {y : α} : ¬✓{n} (some x • some y)

theorem plainly_pure {φ} : ■ ⌜φ⌝ ⊣⊢ (⌜φ⌝ : PROP)

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

theorem persistently_and_emp_elim {P : PROP} [BI PROP] : emp ∧ <pers> P ⊢ P

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

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

theorem core_eq_self {x : α} [IsTotal α] [c : CoreId x] : core x = x

theorem pcore_op_right_L {x cx : α} (h : pcore x = some cx) : x • cx = x

theorem apply_forall [BI PROP] (x : α) (P : α → PROP) {Q : PROP}
    [H1 : IntoForall Q P] (H2 : E ⊢ E' ∗ Q) : E ⊢ E' ∗ P x

theorem inc_iff (ea : (a : α) ≡ a') (eb : (b : α) ≡ b') : a ≼ b ↔ a' ≼ b'

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

theorem affinelyIf_of_intuitionisticallyIf {p : Bool} [BI PROP] {P : PROP} : □?p P ⊢ <affine>?p P

theorem wand_rfl [BI PROP] {P : PROP} : ⊢ P -∗ P

theorem def_eq [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ □ Q

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

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

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

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

theorem LimitPreserving.and [COFE α] {P Q : α → Prop}  (HP : LimitPreserving P)
    (HQ : LimitPreserving Q) : LimitPreserving fun a => P a ∧ Q a

theorem UpdateP.prod' (P : α → Prop) (Q : β → Prop) (x : α × β)
    (uxp : x.fst ~~>: P) (uxq : x.snd ~~>: Q) : x ~~>: λ y ↦ P (y.fst) ∧ Q (y.snd)

theorem or_intro_l' [BI PROP] {P Q R : PROP} (h : P ⊢ Q) : P ⊢ Q ∨ R

protected theorem Hom.valid [CMRA β] (f : α -C> β) {x : α} (H : ✓ x) : ✓ f x

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

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

theorem included_dist_l {n} {x1 x2 x1' : α} :
    x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2

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

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

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

theorem Iso.inv_dist [OFE α] [OFE β] (iso : Iso α β) {n} ⦃x y⦄ :
    x ≡{n}≡ y ↔ iso.inv x ≡{n}≡ iso.inv y

theorem plainly_entails_l (H : P ⊢ ■ Q) : P ⊢ ■ Q ∗ P

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

theorem affinelyIf_flag_mono {p q : Bool} [BI PROP] {P : PROP} (h : q → p) :
    <affine>?p P ⊢ <affine>?q P

theorem intuitionistically_intro' [BI PROP] {P Q : PROP} (h : □ P ⊢ Q) : □ P ⊢ □ Q

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

theorem Agree.op_ne {x : Agree α} : OFE.NonExpansive x.op

theorem Fix.unfold_fold (X : F (Fix F) (Fix F)) : Fix.unfold (Fix.fold X) ≡ X

theorem opM_right_dist {n} (x : α) {y z : Option α} (e : y ≡{n}≡ z) : x •? y ≡{n}≡ x •? z

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

theorem op_core_left_of_inc {x y : α} [CoreId x] (le : x ≼ y) : y • x ≡ y

theorem Agree.op_comm {x y : Agree α} :  x.op y ≡ y.op x

theorem Dist.lt [OFE α] {m n} {x y : α} : x ≡{n}≡ y → m < n → x ≡{m}≡ y

theorem invalid_included [OFE α] (ea : Excl α) : ea ≼ invalid

theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop}
    [h : FromPure true Q φ] [Affine P] (hφ : φ) : P ⊢ Q

theorem incN_iff (ea : (a : α) ≡{n}≡ a') (eb : (b : α) ≡{n}≡ b') : a ≼{n} b ↔ a' ≼{n} b'

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)

@[simp] theorem intuitionisticallyIf_true [BI PROP] (P : PROP) : iprop(□?true P) = iprop(□ P)

theorem wand_elim_r [BI PROP] {P Q : PROP} : P ∗ (P -∗ Q) ⊢ Q

theorem IsoFunStore.store_eq_of_Equiv [Store T K V] [IsoFunStore T K V] {t1 t2 : T}
    (H : Store.Equiv t1 t2) : t1 = t2

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

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

theorem validN_of_incN_validN {a b : α} (Hv : ✓{n} a) (Hinc : some b ≼{n} some a) : ✓{n} b

theorem and_left_comm [BI PROP] {P Q R : PROP} : P ∧ Q ∧ R ⊣⊢ Q ∧ P ∧ R

theorem LeibnizO.dist_inj {x y : α} {n} (H : LeibnizO.mk x ≡{n}≡ LeibnizO.mk y) : x = y

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

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

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

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

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

theorem exact_intuitionistic [BI PROP] (Q : PROP) : □ Q ⊢ Q

theorem multiple' [BI PROP] (P Q R S : PROP) : ⊢ (P -∗ Q) -∗ P -∗ R -∗ (Q -∗ R -∗ S) -∗ S

theorem LocalUpdate.op_discrete [CMRA.Discrete α] (x y z : α)
    (h : ✓ x → ✓ (z • x)) : (x, y) ~l~> (z • x, z • y)

theorem simple [BI PROP] : ⊢ (emp : PROP)

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

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

theorem persistent_and_affinely_sep_l_1 [BI PROP] {P Q : PROP} [Persistent P] :
    P ∧ Q ⊢ <affine> P ∗ Q

theorem bupd_exist {A : Type} {Φ : A → PROP} : (∃ x : A, |==> Φ x) ⊢ |==> ∃ x : A, Φ x

theorem intuitionistically_sep_dup [BI PROP] {P : PROP} : □ P ⊣⊢ □ P ∗ □ P

@[simp] theorem Hom.id_apply [OFE α] {x} : (Hom.id : α -n> α) x = x

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

theorem UpdateP.option {P : α → Prop} {Q : Option α → Prop} {x : α}
    (uxp : x ~~>: P) (pq : ∀ y, P y → Q (some y)) : some x ~~>: Q

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

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

theorem intuitionisticallyIf_or (p : Bool) [BI PROP] {P Q : PROP} : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q

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

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

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

theorem Iso.hom_dist [OFE α] [OFE β] (iso : Iso α β) {n} ⦃x y⦄ :
    x ≡{n}≡ y ↔ iso.hom x ≡{n}≡ iso.hom y

theorem forall_intro [BI PROP] {P : PROP} {Ψ : α → PROP} (h : ∀ a, P ⊢ Ψ a) : P ⊢ ∀ a, Ψ a

theorem pure [BI PROP] : ⊢ (⌜∃ x, x ∨ False⌝ : PROP)

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

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

theorem LocalUpdate.op_frame (x y x' y' yf : α)
    (h : (x, y) ~l~> (x', y')) : (x, y • yf) ~l~> (x', y' • yf)

theorem LocalUpdate.equiv_right (x : α × α) {y z : α × α} (h : y ≡ z) : x ~l~> y → x ~l~> z

theorem DFrac.update_acquire [IsSplitFraction F] :
    (.discard : DFrac F) ~~>: fun k => ∃ q, k = .own q

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

theorem later_iff [BI PROP] {P Q : PROP} : ▷ (P ↔ Q) ⊢ (▷ P ↔ ▷ Q)

theorem absorbinglyIf_and_1 {p : Bool} [BI PROP] {P Q : PROP} :
    <absorb>?p (P ∧ Q) ⊢ <absorb>?p P ∧ <absorb>?p Q

theorem UpdateP.op' {P Q : α → Prop} {x y : α} (uxp : x ~~>: P) (uyq : y ~~>: Q) :
    (x • y : α) ~~>: λ t ↦ ∃ z w, t = (z • w : α) ∧ P z ∧ Q w

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

theorem plainly_emp : ■ emp ⊣⊢ (emp : PROP)

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

theorem pcore_op_left_L {x cx : α} (h : pcore x = some cx) : cx • x = x

theorem _root_.Iris.OFE.Equiv.inc_l : (a : α) ≡ b → (a ≼ c ↔ b ≼ c)

theorem true_intro [BI PROP] {P : PROP} : P ⊢ True

theorem UpdateP.total [CMRA.IsTotal α] :
    x ~~>: P ↔ ∀ (n : Nat) (z : α), ✓{n} (x • z) → ∃ y, P y ∧ ✓{n} (y • z)

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

theorem Contractive.succ [OFE α] [OFE β] (f : α → β) [Contractive f] {n x y}
    (h : x ≡{n}≡ y) : f x ≡{n.succ}≡ f y

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

theorem wand_spatial_multiple [BI PROP] (Q : PROP) : ⊢ P1 -∗ P2 -∗ (P1 -∗ P2 -∗ Q) -∗ Q

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

theorem not_valid_of_exclN_inc {n} {x : α} [Exclusive x] {y} : x ≼{n} y → ¬✓{n} y

theorem some_op_opM {a : α} {ma : Option α} : some a • ma = some (a •? ma)

theorem true_imp [BI PROP] {P : PROP} : (True → P) ⊣⊢ P

theorem Agree.op_comm {x y : Agree α} :  x.op y ≡ y.op x

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

theorem Heap.point_get_eq [Heap T K V] (H : k = k') : get (point k v : T) k' = v

theorem _root_.Option.Forall₂.equivalence {R : α → α → Prop}
    (H : Equivalence R) : Equivalence (Option.Forall₂ R)

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

theorem _root_.Iris.OFE.Dist.incN_l : (a : α) ≡{n}≡ b → (a ≼{n} c ↔ b ≼{n} c)

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

theorem disjoint_union {a b c : State Val} : a |

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

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

theorem later_impl [BI PROP] {P Q : PROP} : ▷ (P → Q) ⊢ ▷ P → ▷ Q

theorem Agree.op_commN {x y : Agree α} :  x.op y ≡{n}≡ y.op x

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

theorem and_exists_l [BI PROP] {P : PROP} {Ψ : α → PROP} : P ∧ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∧ Ψ a

theorem valid_op_right (x y : α) : ✓ (x • y) → ✓ y

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

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

theorem chain_none_const [OFE V] {c : Chain (Option V)} (H : c n = none) :
    c = Chain.const none

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

theorem plainly_entails_r (H : P ⊢ ■ Q) : P ⊢ P ∗ ■ Q

theorem absorbingly_true [BI PROP] : <absorb> True ⊣⊢ (True : PROP)

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

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

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

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

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

theorem plainly_idemp : ■ ■ P ⊣⊢ ■ P

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

<local_ctx>
import Iris.Algebra.CMRA

namespace Iris

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

infixr:50 " ~l~> " => LocalUpdate

section localUpdate

section CMRA

variable [CMRA α]

end CMRA

section UCMRA

variable [UCMRA α]
</local_ctx>

<target_theorem>
theorem local_update_unital_discrete [CMRA.Discrete α] (x y x' y' : α) :
    (x, y) ~l~> (x', y') ↔ ∀ z, ✓ x → x ≡ y • z → (✓ x' ∧ x' ≡ y' • z) :=
</target_theorem>

