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 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)

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 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 IsModal [BI PROP1] [BI PROP2] (M : PROP1 → PROP2)
    (iaction saction : ModalityAction PROP1 PROP2) where
  spec_intuitionistic : iaction.intuitionistic_action_spec M
  spec_spatial : saction.spatial_action_spec M
  emp : iprop(emp) ⊢ M iprop(emp)
  mono : ∀ {P Q}, (P ⊢ Q) → M P ⊢ M Q
  sep : ∀ {P Q}, iprop(M P ∗ M Q) ⊢ M iprop(P ∗ Q)

@[ext]
structure UPred (M : Type _) [UCMRA M] where
  holds : Nat → M → Prop
  mono {n1 n2 x1 x2} : holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → holds n2 x2

instance : OFE (Tower F) where
  Equiv f g := ∀ k, f k ≡ g k
  Dist n f g := ∀ k, f k ≡{n}≡ g k
  dist_eqv := {
    refl _ _ := dist_eqv.refl _
    symm h _ := dist_eqv.symm (h _)
    trans h1 h2 _ := dist_eqv.trans (h1 _) (h2 _)
  }
  equiv_dist {_ _} := by admit /- proof elided -/

class BIPlainly (PROP : Type _) [Iris.BI PROP] extends Plainly PROP where
  [ne : Iris.OFE.NonExpansive (Plainly.plainly (PROP := PROP))]
  mono {P Q : PROP} : (P ⊢ Q) → ■ P ⊢ ■ Q
  elim_persistently {P : PROP} : ■ P ⊢ <pers> P
  idem {P : PROP} : ■ P ⊢ ■ ■ P
  plainly_sForall_2 {Φ : PROP → Prop} : (∀ p, ⌜Φ p⌝ → ■ p) ⊢ ■ sForall Φ
  plainly_impl_plainly {P Q : PROP} : (■ P → ■ Q) ⊢ ■ (■ P → Q)
  emp_intro {P : PROP} : P ⊢ ■ emp
  plainly_absorb {P Q : PROP} : ■ P ∗ Q ⊢ ■ P
  later_plainly {P : PROP} : ▷ ■ P ⊣⊢ ■ ▷ P

@[simp] def Store.Equiv [Store T K V] (t1 t2 : T) : Prop := get t1 = get t2

instance Store.Equiv_trans [Store T K V] : Trans Equiv (Equiv (T := T)) Equiv := ⟨by admit /- proof elided -/
⟩

protected def later (P : UPred M) : UPred M where
  holds n x := match n with | 0 => True | Nat.succ n' => P n' x
  mono {n₁ n₂} := by admit /- proof elided -/

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

instance later_contractive : OFE.Contractive UPred.later (α := UPred M) where
  distLater_dist {n x y} Hl :=
    match n with
    | 0 => by admit /- proof elided -/
    | n + 1 => fun
      | 0 => by admit /- proof elided -/
      | n' + 1 => fun x' Hn' Hx' => Hl _ Hn' _ _ (Nat.le_refl _) (CMRA.validN_succ Hx')

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

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 OFE.ContractiveHom.fixpoint_ne [COFE α] [Inhabited α] :
    NonExpansive (ContractiveHom.fixpoint (α := α)) where
  ne n f1 f2 H := by admit /- proof elided -/

instance instOFE [Store T K V] [OFE V] : OFE T where
  Equiv s0 s1  := get s0 ≡ get s1
  Dist n s0 s1 := get s0 ≡{n}≡ get s1
  dist_eqv     := ⟨fun _ => .of_eq rfl, (·.symm), (·.trans ·)⟩
  equiv_dist   := equiv_dist
  dist_lt      := dist_lt

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 [Store T1 K V1] [Store T2 K V2] [OFE V1] [OFE V2] (f : K → V1 → V2)
  [∀ k, NonExpansive (f k)] [HasStoreMap T1 T2 K V1 V2] : NonExpansive (dmap f : T1 → T2) where
  ne _ {_ _} H k := by admit /- proof elided -/

instance Heap.instCOFE [Heap T K V] [COFE V] : COFE T where
  compl c := hmap (fun _ => COFE.compl <| c.map ⟨_, Store.get_ne ·⟩) (c 0)
  conv_compl {_ c} k := by admit /- proof elided -/

class BIUpdate (PROP : Type _) [BI PROP] extends BUpd PROP where
  [bupd_ne : OFE.NonExpansive (BUpd.bupd (PROP := PROP))]
  intro {P : PROP} : iprop(P ⊢ |==> P)
  mono {P Q : PROP} : iprop(P ⊢ Q) → iprop(|==> P ⊢ |==> Q)
  trans {P : PROP} : iprop(|==> |==> P ⊢ |==> P)
  frame_r {P R : PROP} : iprop((|==> P) ∗ R ⊢ |==> (P ∗ R))

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

instance : OFE.Discrete (DFrac F) := ⟨congrArg id⟩

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 UCMRA (α : Type _) extends CMRA α where
  unit : α
  unit_valid : ✓ unit
  unit_left_id : unit • x ≡ x
  pcore_unit : pcore unit ≡ some unit

instance [CMRA β] : OFE (α -C> β) where
  Equiv f g := f.toHom ≡ g.toHom
  Dist n f g := f.toHom ≡{n}≡ 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

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

partial def iIntroCore
    {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List iCasesPat)
    (k : ∀ {P}, Hyps bi P → (Q : Q($prop)) → MetaM Q($P ⊢ $Q)) :
    MetaM (Q($P ⊢ $Q)) := do
  match pats with
  | [] => k hyps Q
  | pat :: pats =>
    let A1 ← mkFreshExprMVarQ q($prop)
    let A2 ← mkFreshExprMVarQ q($prop)
    let fromImp ← try? (α := Q(FromImp $Q $A1 $A2)) do
      synthInstanceQ q(FromImp $Q $A1 $A2)
    if let (.clear, some _) := (pat, fromImp) then
      let pf ← iIntroCore hyps A2 pats k
      return q(imp_intro_drop (Q := $Q) $pf)
    else
    let alres ← try? (α := _ × (v : Level) × (α : Q(Sort v)) × (Φ : Q($α → $prop)) ×
        Q(FromForall $Q $Φ)) do
      let .one n := pat | failure
      let v ← mkFreshLevelMVar
      let α ← mkFreshExprMVarQ q(Sort v)
      let Φ ← mkFreshExprMVarQ q($α → $prop)
      Pure.pure ⟨n, v, α, Φ, ← synthInstanceQ q(FromForall $Q $Φ)⟩
    if let some ⟨n, _, α, Φ, _⟩ := alres then
      let (n, ref) ← getFreshName n
      withLocalDeclDQ n α fun x => do
        addLocalVarInfo ref (← getLCtx) x α
        have B : Q($prop) := Expr.headBeta q($Φ $x)
        have : $B =Q $Φ $x := ⟨⟩
        let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← iIntroCore hyps B pats k
        return q(from_forall_intro (Q := $Q) $pf)
    else
    let B ← mkFreshExprMVarQ q($prop)
    match pat, fromImp with
    | .intuitionistic pat, some _ =>
      let _ ← synthInstanceQ q(IntoPersistently false $A1 $B)
      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore · A2 pats k)
      return q(imp_intro_intuitionistic (Q := $Q) $pf)
    | .intuitionistic pat, none =>
      let _ ← synthInstanceQ q(FromWand $Q $A1 $A2)
      let _ ← synthInstanceQ q(IntoPersistently false $A1 $B)
      let _ ← synthInstanceQ q(TCOr (Affine $A1) (Absorbing $A2))
      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore · A2 pats k)
      return q(wand_intro_intuitionistic (Q := $Q) $pf)
    | _, some _ =>
      let _ ← synthInstanceQ q(FromAffinely $B $A1)
      let _ ← synthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P))
      let pf ← iCasesCore bi hyps A2 q(false) B B ⟨⟩ pat (iIntroCore · A2 pats k)
      return q(imp_intro_spatial (Q := $Q) $pf)
    | _, none =>
      let _ ← synthInstanceQ q(FromWand $Q $A1 $A2)
      let pf ← iCasesCore bi hyps A2 q(false) A1 A1 ⟨⟩ pat (iIntroCore · A2 pats k)
      return q(wand_intro_spatial (Q := $Q) $pf)

structure RemoveHyp {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where
  (e' : Q($prop)) (hyps' : Hyps bi e') (out out' : Q($prop)) (p : Q(Bool))
  (eq : $out =Q iprop(□?$p $out'))
  (pf : Q($e ⊣⊢ $e' ∗ $out))
  deriving Inhabited

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

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

Equivalence in Init.Core

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 ..

def Heap.dom [Heap T K V] (t : T) : K → Prop := fun k => (get t k).isSome

Unit in Init.Prelude

instance [BI PROP] : RightId (α := PROP) BiEntails iprop(True) and := ⟨and_true⟩

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

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

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

inductive ReplaceHyp {prop : Q(Type u)} (bi : Q(BI $prop)) (Q : Q($prop)) where
  | none
  | unchanged (ehyps') (hyps' : Hyps bi ehyps')
  | main (e e' : Q($prop)) (hyps' : Hyps bi e') (pf : Q(Replaces $Q $e $e'))

def GName := LeibnizO Nat

partial def instantiateForalls {prop : Q(Type u)} (bi : Q(BI $prop)) (hyp : Q($prop))
    (pf : Q(⊢ $hyp)) (terms : List Term) : TacticM (Expr × Expr) := do
  if let some t := terms.head? then
    let texpr ← mkAppM' (← elabTerm t none) #[]
    let ⟨_, ttype, texpr⟩ ← inferTypeQ texpr
    let Φ ← mkFreshExprMVarQ q($ttype → $prop)
    let _ ← synthInstanceQ q(IntoForall $hyp $Φ)
    let res ← mkAppM' Φ #[texpr]
    let pf' ← mkAppM ``pose_forall #[texpr, Φ, pf]
    return ← instantiateForalls bi res pf' terms.tail
  else
    let pf ← mkAppM ``as_emp_valid_1 #[hyp, pf]
    return ⟨hyp, pf⟩

instance (priority := default + 20) intoPersistently_affinely (p : Bool) [BI PROP] (P Q : PROP)
    [h : IntoPersistently p P Q] : IntoPersistently p iprop(<affine> P) Q where
  into_persistently := (persistentlyIf_mono affinely_elim).trans h.1

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

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

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

instance : Inhabited (Tower F) := ⟨Tower.embed 0 ⟨()⟩⟩

def addLocalVarInfo (stx : Syntax) (lctx : LocalContext)
    (expr : Expr) (expectedType? : Option Expr) (isBinder := false) : MetaM Unit := do
  Elab.withInfoContext' (pure ())
    (fun _ =>
      return .inl <| .ofTermInfo
        { elaborator := .anonymous, lctx, expr, stx, expectedType?, isBinder })
    (return .ofPartialTermInfo { elaborator := .anonymous, lctx, stx, expectedType? })

instance affinelyIf_affine (p : Bool) [BI PROP] (P : PROP) [Affine P] :
    Affine iprop(<affine>?p P) :=

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

@[ext] structure Hom (α β : Type _) [CMRA α] [CMRA β] extends OFE.Hom α β where
  protected validN {n x} : ✓{n} x → ✓{n} (f x)
  protected pcore x : (pcore x).map f ≡ pcore (f x)
  protected op x y : f (x • y) ≡ f x • f y

Lean.Parser.Term.matchAlts in Lean.Parser.Term

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

instance intoOr_pure (φ ψ : Prop) [BI PROP] :
    IntoOr (PROP := PROP) iprop(⌜φ ∨ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝) where
  into_or := pure_or.2

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

local instance : OFE.NonExpansive (Agree.map' f) where
  ne := by admit /- proof elided -/

def selectHyp (ty : Expr) : ∀ {s}, @Hyps u prop bi s → MetaM (Name × Q(Bool) × Q($prop))
  | _, .emp _ => failure
  | _, .hyp _ _ uniq p ty' _ => do
    let .true ← isDefEq ty ty' | failure
    pure (uniq, p, ty')
  | _, .sep _ _ _ _ lhs rhs => try selectHyp ty rhs catch _ => selectHyp ty lhs

instance false_affine [BI PROP] : Affine (PROP := PROP) iprop(False) where
  affine := false_elim

instance intoOr_affinely [BI PROP] (P Q1 Q2 : PROP) [h : IntoOr P Q1 Q2] :
    IntoOr iprop(<affine> P) iprop(<affine> Q1) iprop(<affine> Q2) where
  into_or := (affinely_mono h.1).trans affinely_or.1

class CoreId (x : α) where
  core_id : pcore x ≡ some x

def SubG (FF₁ FF₂ : GFunctors) : Prop :=
  ∀ i : GId FF₁, ∃ j : GId FF₂, FF₁[i] = FF₂[j]

instance (priority := default + 10) fromSep_persistently [BI PROP] (P Q1 Q2 : PROP)
    [h : FromSep P Q1 Q2] : FromSep iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2) where
  from_sep := persistently_sep_2.trans (persistently_mono h.1)

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

instance {m : T} [Hid : ∀ x : V, IdFree x] [Hc : ∀ x : V, Cancelable x] : Cancelable m where
  cancelableN {n m1 m2} Hv He i := by admit /- proof elided -/

class FromWand [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
  from_wand : (Q1 -∗ Q2) ⊢ P

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

instance : BIPlainlyExists (UPred M) where
  plainly_sExists_1 _ _ _ := fun ⟨_, hp⟩ => ⟨_, ⟨_, rfl⟩, hp⟩

instance (priority := default + 20) intoPersistently_intuitionistically (p : Bool) [BI PROP]
    (P Q : PROP) [h : IntoPersistently true P Q] : IntoPersistently p iprop(□ P) Q where
  into_persistently := persistentlyIf_intutitionistically.trans h.1

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 -/

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

inductive RewriteModifier
  | single
  | all

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

def HypMarker {PROP : Type _} (_A : PROP) : Prop := True

def ownM (m : M) : UPred M where
  holds n x := m ≼{n} x
  mono {n₁ n₂ x₁ x₂} := fun ⟨m₁, Hm₁⟩ ⟨m₂, Hm₂⟩ Hn => by admit /- proof elided -/

let (name, ref) ← getFreshName name
  withLocalDeclDQ name φ fun p => do
    addLocalVarInfo ref (← getLCtx) p φ
    let (a, m) ← k φ p
    let f : Q($φ → $P' ⊢ $Q) ← mkLambdaFVars #[p] m

instance intoWand_imp_true [BI PROP] (P Q P' : PROP) [Affine P']
    [h : FromAssumption b P P'] : IntoWand true 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 intuitionistically_elim

partial def parseHyps? {prop : Q(Type u)} (bi : Q(BI $prop)) (expr : Expr) :
    Option ((s : Q($prop)) × Hyps bi s) := do
  if let some #[_, _, P, Q] := appM? expr ``sep then
    let ⟨elhs, lhs⟩ ← parseHyps? bi P
    let ⟨erhs, rhs⟩ ← parseHyps? bi Q
    some ⟨q(BI.sep $elhs $erhs), .sep expr elhs erhs ⟨⟩ lhs rhs⟩
  else if expr.isAppOfArity ``emp 2 then
    some ⟨expr, .emp ⟨⟩⟩
  else if let some #[_, _, P] := appM? expr ``intuitionistically then
    let (name, uniq, (ty : Q($prop))) ← parseName? P
    some ⟨q(iprop(□ $ty)), .hyp expr name uniq q(true) ty ⟨⟩⟩
  else
    let (name, uniq, ty) ← parseName? expr
    some ⟨ty, .hyp expr name uniq q(false) ty ⟨⟩⟩

def assumptionSlow (assume : Bool) :
    ∀ {e}, Hyps bi e → MetaM (AssumptionSlow bi Q e)
  | _, .emp _ =>
    Pure.pure (.affine q(emp_affine))
  | out, .hyp _ _ _ b ty _ => do
    let fromAssum (_:Unit) := do
      let _ ← synthInstanceQ q(FromAssumption $b $ty $Q)
      let inst ← try? (synthInstanceQ q(Affine $out))
      return .main q(FromAssumption.from_assumption) inst
    let affine (_:Unit) := return .affine (← synthInstanceQ q(Affine $out))
    if assume then
      try fromAssum () catch _ => try affine () catch _ => return .none
    else
      try affine () catch _ => try fromAssum () catch _ => return .none
  | _, .sep _ elhs erhs _ lhs rhs => do
    match ← assumptionSlow assume rhs with
    | .none => return .none
    | .affine _ =>
      match ← assumptionSlow assume lhs with
      | .none => return .none
      | .affine _ => return .affine q(sep_affine ..)
      | .main lpf linst =>
        return .main q(assumption_l $lpf) <| linst.map fun _ => q(sep_affine $elhs $erhs)
    | .main rpf rinst =>
      match ← assumptionSlow false lhs, rinst with
      | .none, _ | .main _ none, none => return .none
      | .affine _, rinst | .main _ (some _), rinst =>
        return .main q(assumption_r $rpf) <| rinst.map fun _ => q(sep_affine $elhs $erhs)
      | .main lpf none, some _ => return .main q(assumption_l $lpf) none

instance : OFE.NonExpansive (bupd : UPred M → UPred M) where
  ne {n} {x1 x2} H {n' x'} Hn' Hx' := by admit /- proof elided -/

instance [BI PROP] : LawfulBigOp sep (emp : PROP) BiEntails where
  refl := .rfl
  symm h := h.symm
  trans h1 h2 := h1.trans h2
  comm := sep_comm
  assoc := sep_assoc
  left_id := emp_sep
  congr_l := sep_congr_l

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

Option.elim in Init.Data.Option.Basic

instance [CMRA α] : Trans Update Update Update (α := α) where
  trans := Update.trans

Qq.synthInstanceQ in Qq.MetaM

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

instance fromOr_affinely [BI PROP] (P Q1 Q2 : PROP) [h : FromOr P Q1 Q2] :
    FromOr iprop(<affine> P) iprop(<affine> Q1) iprop(<affine> Q2) where
  from_or := affinely_or.2.trans (affinely_mono h.1)

Exists in Init.Core

def uliftUpHom [OFE α] : α -n> ULift α where
  f := .up
  ne.1 _ _ _ := id

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)

def core (x : α) := (pcore x).getD x

instance : Inhabited (QuotedDefEq a b) := ⟨⟨⟩⟩

def except0 [BIBase PROP] (P : PROP) := iprop(▷ False ∨ P)

instance intoOr_persistently [BI PROP] (P Q1 Q2 : PROP) [h : IntoOr P Q1 Q2] :
    IntoOr iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2) where
  into_or := (persistently_mono h.1).trans persistently_or.1

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

Nat.eq_or_lt_of_le in Init.Prelude

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

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

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

protected def wand (P Q : UPred M) : UPred M where
  holds n x := ∀ n' x', n' ≤ n → ✓{n'} (x • x') → P n' x' → Q n' (x • x')
  mono {n₁ n₂ m₁ m₂} H Hm Hn n' x Hn' Hv HP := by admit /- proof elided -/

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

Lean.KVMap in Lean.Data.KVMap

inductive RemoveHypCore {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) (α : Type) where
  | none
  | one (a : α) (out' : Q($prop)) (p : Q(Bool)) (eq : $e =Q iprop(□?$p $out'))
  | main (a : α) (_ : RemoveHyp bi e)

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 RightId (R : Relation α) (i : α) (f : α → α → α) where
  right_id {x : α} : R (f x i) x

instance [OFE α] [Leibniz α] : Leibniz (Option α) where
  eq_of_eqv {x y} H :=
    match x, y, H with
    | none, none, _ => rfl
    | some _, some _, h => congrArg some (Leibniz.eq_of_eqv h)

instance OFunctor.constOF_RFunctorContractive [CMRA B] :
    RFunctorContractive (COFE.constOF B) where
  map_contractive.1 := by admit /- proof elided -/

def chain_option_some [OFE V] {c : Chain (Option V)} (H : c n = some v) :
    ∃ c' : Chain V, c = Chain.map ⟨some, OFE.Option.some.ne⟩ c' :=

unif_hint (b : Bool) where
  |- false || b ≟ b
unif_hint (b : Bool) where
  |- true || b ≟ true
unif_hint (b : Bool) where
  |- false && b ≟ false
unif_hint (b : Bool) where
  |- true && b ≟ b

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 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 intoWand_persistently_true (q : Bool) [BI PROP] (R P Q : PROP)
    [h : IntoWand true q R P Q] : IntoWand true q iprop(<pers> R) P Q where
  into_wand := intuitionistically_persistently.1.trans h.1

def exclO_map [OFE α] [OFE β] (f : α -n> β) : Excl α -C> Excl β :=

instance forall_absorbing [BI PROP] (Φ : α → PROP) [∀ x, Absorbing (Φ x)] :
    Absorbing iprop(∀ x, Φ x) where
  absorbing := absorbingly_forall_1.trans (forall_mono fun _ => absorbing)

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

instance fromOr_absorbingly [BI PROP] (P Q1 Q2 : PROP) [h : FromOr P Q1 Q2] :
    FromOr iprop(<absorb> P) iprop(<absorb> Q1) iprop(<absorb> Q2) where
  from_or := absorbingly_or.2.trans (absorbingly_mono h.1)

Lean.Parser.Term.leading_parser in Lean.Parser.Term

instance URFunctor.toRFunctor [UF : URFunctor F] : RFunctor F where
  cmra     := URFunctor.cmra.toCMRA
  map f g  := URFunctor.map f g
  map_ne   := URFunctor.map_ne
  map_id   := URFunctor.map_id
  map_comp := URFunctor.map_comp

@[ext]
structure Agree where
  car : List α
  not_nil : car ≠ []

instance (P : UPred M) : Affine P where
  affine _ := by admit /- proof elided -/

instance fromPure_emp [BI PROP] : FromPure (PROP := PROP) true emp True where
  from_pure := affinely_true.1

instance (priority := default + 10) fromAssumption_forall (p : Bool) [BI PROP] (Φ : α → PROP)
    (x : α) (Q : PROP) [h : FromAssumption p (Φ x) Q] : FromAssumption p iprop(∀ x, Φ x) Q where
  from_assumption := (intuitionisticallyIf_mono <| forall_elim x).trans h.1

instance (priority := default - 50) fromAffinely_affinely [BI PROP] (P : PROP) :
    FromAffinely iprop(<affine> P) P true := ⟨.rfl⟩

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)

def Fractional [Fraction α] (a : α) : Prop := ∃ b, Proper (a + b)

let m1 : Q($el ⊢ $Q1) ← mkFreshExprSyntheticOpaqueMVar <|
    IrisGoal.toExpr { u, prop, bi, hyps := lhs, goal := Q1, .. }
  let m2 : Q($er ⊢ $Q2) ← mkFreshExprSyntheticOpaqueMVar <|
    IrisGoal.toExpr { u, prop, bi, hyps := rhs, goal := Q2, .. }
  mvar.assign q(sep_split (Q := $goal) $pf $m1 $m2)
  replaceMainGoal [m1.mvarId!, m2.mvarId!]

Lean.Level in Lean.Level

class FromExists [BI PROP] (P : PROP) {α : outParam (Sort _)} (Φ : outParam <| α → PROP) where
  from_exists : (∃ x, Φ x) ⊢ P

instance [t : T] : TCIte (no_index true) T U := TCIte.t (t := t)

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

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

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

Lean.Elab.Tactic.evalTactic in Lean.Elab.Tactic.Basic

def unfoldChain (X : Tower F) : Chain (F (Tower F) (Tower F)) where
  chain n := map (Tower.proj _) (Tower.embed _) (X (n+1))
  cauchy {n i} h := by admit /- proof elided -/

ULift in Init.Prelude

@[simp]
def MyAg (S : String) : Agree (LeibnizO String) := ⟨[⟨S⟩], by admit /- proof elided -/
⟩

CoeFun in Init.Coe

instance idFree_op_l {x y : α} [IdFree x] [Cancelable y] : IdFree (x • y) :=
  comm.idFree.1 inferInstance

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

m in QqTest.matching

let _ ← isDefEq er goal
  if let (some _, some _) := (← try? <| synthInstanceQ q(FromAssumption false $er $goal),
                              ← try? <| synthInstanceQ q(TCOr (Affine $el) (Absorbing $goal))) then
    
    return q(assumption (p := false) .rfl)
  else if let some _ ← try? <| synthInstanceQ q(IntoWand false false $er $A1 $goal) then
    
    let m ← specPatGoal A1 hypsl spats addGoal
    return q(apply $m)
  else if let some _ ← try? <| synthInstanceQ q(IntoWand false false $er $A1 $A2) then
    
    let ⟨el', _, m, hypsl', h'⟩ ← processSpecPats A1 hypsl spats addGoal
    let res : Q($el' ∗ $A2 ⊢ $goal) ← iApplyCore goal el' A2 hypsl' spats.tail addGoal
    return q(rec_apply $h' $m $res)
  else
    throwError "iapply: cannot apply {er} to {goal}"

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

instance DFrac_CMRA : CMRA (DFrac F) where
  pcore := pcore
  op := op
  Valid := valid
  ValidN _ := valid
  op_ne := { ne _ _ _ := congrArg (op _) }
  pcore_ne {_} := by admit /- proof elided -/

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

Qq.mkFreshExprMVarQ in Qq.MetaM

Lean.mkApp in Lean.Expr

Id.run in Init.Control.Id

Prod in Init.Prelude
</all_available_defs>

<all_available_lemmas>
theorem persistently_elim_plainly : <pers> ■ P ⊣⊢ ■ P

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

theorem validN_op_opM_left {mz : Option α} : ✓{n} (x • y : α) •? mz → ✓{n} x •? mz

theorem intuitionistically_ne [BI PROP] : OFE.NonExpansive (@intuitionistically PROP _)

theorem set_op_equiv {m1 m2 : T} :
    Equiv ((set (V := Option V) (m1 • m2) i (x • y))) (set m1 i x • set m2 i y)

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

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

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

theorem sep_and_elim_l [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2]
    (h : P ∗ □?p A1 ⊢ Q) : P ∗ □?p A ⊢ Q

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

theorem affinely_absorbingly [BI PROP] [BIPositive PROP] {P : PROP} :
    <affine> <absorb> P ⊣⊢ <affine> P

theorem core_idem (x : α) : core (core x) ≡ core x

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

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

theorem cmraValid_entails [CMRA A] [CMRA B] {a : A} {b : B} (Hv : ∀ n, ✓{n} a → ✓{n} b) :
    (cmraValid a : UPred M) ⊢ cmraValid b

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

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

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

theorem exists_elim [BI PROP] {Φ : α → PROP} {Q : PROP} (h : ∀ a, Φ a ⊢ Q) : (∃ a, Φ a) ⊢ 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 Update.discrete_total [CMRA.Discrete α] [CMRA.IsTotal α] :
    x ~~> y ↔ ∀ (z : α), ✓ (x • z) → ✓ (y • z)

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

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

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

theorem pure [BI PROP] (P : PROP) (HF : False) : ⊢ P

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

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

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

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

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

theorem exact_lean'' [BI PROP] (Q : PROP) (H : 0 = 0 → ⊢ Q) : ⊢ Q

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

theorem op_opM_cancel_dist {x y z : α} [Cancelable x]
    (vxy : ✓{n} x • y) (h : x • y ≡{n}≡ (x • z) •? mw) : y ≡{n}≡ z •? mw

theorem plainly_impl_wand : ■ (P → Q) ⊣⊢ ■ (P -∗ Q)

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

theorem persistently_pure {φ : Prop} [BI PROP] : <pers> ⌜φ⌝ ⊣⊢ (⌜φ⌝ : PROP)

theorem move_to_pure_disjunction [BI PROP] (Q : PROP) :
    ⊢ <affine> ⌜φ1⌝ ∨ <affine> ⌜φ2⌝ -∗ Q -∗ Q

theorem exists_intro' [BI PROP] {P : PROP} {Ψ : α → PROP} (a : α) (h : P ⊢ Ψ a) : P ⊢ ∃ a, Ψ a

theorem valid_discard : ✓ (discard : DFrac F)

theorem sep_and_elim_r [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2]
    (h : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q

theorem and_persistent_right [BI PROP] (Q : PROP) : Q ∧ <pers> P ⊢ Q

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

theorem replaces_l [BI PROP] {K P P' Q : PROP} (h : Replaces K P P') :
    Replaces K iprop(P ∗ Q) iprop(P' ∗ Q)

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

theorem intuitionistically_exists [BI PROP] {Φ : α → PROP} : □ (∃ x, Φ x) ⊣⊢ ∃ x, □ Φ x

theorem valid_of_eqv {x y : α} : x ≡ y → ✓ x → ✓ y

theorem imp_elim_l [BI PROP] {P Q : PROP} : (P → Q) ∧ P ⊢ Q

theorem exists_elim_intuitionistic [BI PROP] {P A Q : PROP} {Φ : α → PROP} [IntoExists A Φ]
    (h : ∀ a, P ∗ □ Φ a ⊢ Q) : P ∗ □ A ⊢ Q

theorem Fractional.of_add_left {a a' : α} (H : Fractional (a + a')) : Fractional a

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

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_emp [BI PROP] [BIAffine PROP] : (▷ emp ⊣⊢ (emp : PROP))

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

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

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

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

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

theorem persistent_and_sep_1 [BI PROP] {P Q : PROP} :
    [TCOr (Persistent P) (Persistent Q)] → P ∧ Q ⊢ P ∗ Q

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

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

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

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

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

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

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

@[rw_mono_rule]
theorem exists_mono [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ⊢ Ψ a) : (∃ a, Φ a) ⊢ ∃ a, Ψ a

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

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

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

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

theorem plainly_intro' (H : ■ P ⊢ Q) : ■ P ⊢ ■ Q

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

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

theorem validN_core {n} {x : α} (v : ✓{n} x) : ✓{n} core x

theorem op_commN {x y : α} : x • y ≡{n}≡ y • x

theorem LocalUpdate.exclusive [CMRA.Exclusive y] {x x' : α}
    (vx' : ✓ x') : (x, y) ~l~> (x', x')

theorem pose_forall [BI PROP] (x : α) (P : α → PROP) {Q : PROP}
    [H1 : IntoForall Q P] (H2 : ⊢ Q) : ⊢ P x

theorem incN_of_incN_succ {n} {x y : α} : x ≼{n.succ} y → x ≼{n} y

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

theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop}
    [h : FromPure false Q φ] (hφ : φ) : P ⊢ Q

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

theorem delete_validN {m : T} (Hv : ✓{n} m) : ✓{n} (delete m i)

theorem intuitionisticallyIf_comm {p q : Bool} [BI PROP] {P : PROP} :
    iprop(□?p □?q P) = iprop(□?q □?p P)

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

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

theorem affinely_exists [BI PROP] {Φ : α → PROP} : <affine> (∃ a, Φ a) ⊣⊢ ∃ a, <affine> (Φ a)

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

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

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

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

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

theorem affinelyIf_idem {p : Bool} [BI PROP] [BIPositive PROP] {P : PROP} :
    <affine>?p <affine>?p P ⊣⊢ <affine>?p P

@[rw_mono_rule]
theorem intuitionisticallyIf_mono {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊢ Q) : □?p P ⊢ □?p Q

theorem assumption_r [BI PROP] {P Q R : PROP} [Affine P] (h : Q ⊢ R) : P ∗ Q ⊢ R

theorem point_inc_iff {m : T} :
    (point i (T := T) (some x)) ≼ m ↔ ∃ y, (get m i ≡ some y) ∧ some x ≼ some y

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

theorem Agree.equiv_def {x y : Agree α} : x ≡ y ↔ ∀ n, Agree.dist n x y

theorem assumption [BI PROP] {p : Bool} {P P' A Q : PROP} [inst : FromAssumption p A Q]
  [TCOr (Affine P') (Absorbing Q)] (h : P ⊣⊢ P' ∗ □?p A) : P ⊢ Q

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

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

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

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

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

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

@[rw_mono_rule]
theorem forall_congr [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ⊣⊢ Ψ a) : (∀ a, Φ a) ⊣⊢ ∀ a, Ψ a

theorem up_down {k} (x) : up F (k+1) (down F (k+1) x) ≡{k}≡ x

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

theorem persistently_exists [BI PROP] {Ψ : α → PROP} : <pers> (∃ a, Ψ a) ⊣⊢ ∃ a, <pers> (Ψ a)

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

theorem point_core_total_eq [IsTotal V] [IsoFunStore T K (Option V)] {i : K} {x : V} :
    core (point (T := T) i (some x)) = point i (some (core x))

theorem plainly_elim [Absorbing P] : ■ P ⊢ P

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

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

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) :
    g y ~~>: λ x ↦ ∃ y, x = g y ∧ P y

theorem LocalUpdate.discrete [CMRA.Discrete α] (x y x' y' : α) :
    (x, y) ~l~> (x', y') ↔ ∀ mz, ✓ x → x ≡ y •? mz → (✓ x' ∧ x' ≡ y' •? mz)

theorem biaffine_of_true_affine [BI PROP] [Affine (iprop(True) : PROP)] : BIAffine PROP

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

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

theorem later_affinely_2 [BI PROP] {P : PROP} : <affine> ▷ P ⊢ ▷ <affine> P

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

theorem Excl.dist_eqv [OFE α] {n} : Equivalence (Excl.Dist (α := α) n)

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 sForall_persistent [BI PROP] [h : BIPersistentlyForall PROP] (Ψ : PROP → Prop)
    (H : ∀ p, Ψ p → Persistent p) : Persistent iprop(sForall Ψ)

theorem some_incN_some_iff_some [IsTotal α] {x y : α} : some y ≼{n} some x → y ≼{n} x

theorem cmra_cmraValid_weaken [CMRA A] (a b : A) :
    (cmraValid (a • b) : UPred M) ⊢ cmraValid a

protected theorem Tower.upN (X : Tower F) : ∀ i, upN F i (X (k+1)) ≡{k}≡ X (k+1+i)

theorem later_intuitionistically [BI PROP] [BIAffine PROP] {P : PROP} : □ ▷ P ⊣⊢ ▷ □ P

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

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

theorem affinely_plainly_elim : <affine> ■ P ⊢ P

theorem intuitionistically_def [BI PROP] {P : PROP} : iprop(□ P) = iprop(<affine> <pers> P)

theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP}
    [FromWand Q A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q

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

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

theorem plainly_and_sep : ■ (P ∧ Q) ⊢ ■ (P ∗ Q)

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

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

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

theorem idFree_iff {x₁ x₂ : α} (e : x₁ ≡ x₂) : IdFree x₁ ↔ IdFree x₂

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

theorem apply [BI PROP] {P Q1 Q2 R : PROP}
    (h : P ⊢ Q1) [inst : IntoWand false false R Q1 Q2] : P ∗ R ⊢ Q2

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

theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP}
    (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ □?p P1)
    [inst : IntoWand q p Q P1 P2] : A1 ⊢ A3 ∗ □?(p && q) P2

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

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

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

theorem _root_.Iris.OFE.Dist.exclusive {x₁ x₂ : α} : x₁ ≡ x₂ → (Exclusive x₁ ↔ Exclusive x₂)

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

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

theorem Agree.op_def {x y : Agree α} : x • y = x.op y

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

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

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

theorem or_emp [BI PROP] {P : PROP} [Affine P] : P ∨ emp ⊣⊢ emp

theorem Agree.included {x y : Agree α} : x ≼ y ↔ y ≡ y • x

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 persistently_and [BI PROP] {P Q : PROP} : <pers> (P ∧ Q) ⊣⊢ <pers> P ∧ <pers> Q

theorem DFrac.is_discrete {q : DFrac F} : OFE.DiscreteE q

theorem true_sep [BI PROP] {P : PROP} [Absorbing P] : True ∗ P ⊣⊢ P

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

theorem loeb_wand_intuitionistically [BI PROP] [BILoeb PROP] {P : PROP} :
    □ (□ ▷ P -∗ P) ⊢ P

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

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

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

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

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

theorem sExists_persistent [BI PROP] (Ψ : PROP → Prop)
    (H : ∀ p, Ψ p → Persistent p) : Persistent iprop(sExists Ψ)

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

<local_ctx>
namespace Iris

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

open OFE

scoped infix:40 " ≡ " => OFE.Equiv

scoped notation:40 x " ≡{" n "}≡ " y:41 => OFE.Dist n x y

namespace OFE
</local_ctx>

<target_theorem>
theorem equiv_eqv [ofe : OFE α] : Equivalence ofe.Equiv :=
</target_theorem>

