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>
@[ext]
structure Agree where
  car : List α
  not_nil : car ≠ []

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)

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

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

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

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

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

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

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

@[ext] structure LeibnizO (α : Type _) where
  car : α

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

class Fraction (α : Type _) extends Add α where
   
  Proper : α → Prop
  add_comm : ∀ a b : α, a + b = b + a
  add_assoc : ∀ a b c : α, a + (b + c) = (a + b) + c
  add_left_cancel : ∀ {a b c : α}, a + b = a + c → b = c
   
  add_ne : ∀ {a b : α}, a ≠ b + a
  proper_add_mono_left : ∀ {a b : α}, Proper (a + b) → Proper a

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

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

def valid : DFrac F → Prop
  | .own f        => Proper f
  | .discard      => True
  | .ownDiscard f => Fractional f

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

abbrev op (x y : α × β) : α × β :=
  (x.1 • y.1, x.2 • y.2)

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

instance fromPure_pure_imp (a : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
    [h1 : IntoPure P1 φ1] [h2 : FromPure a P2 φ2] : FromPure a iprop(P1 → P2) (φ1 → φ2) where
  from_pure := (affinelyIf_mono pure_imp_2).trans <|
    (BI.imp_intro <| affinelyIf_and_l.1.trans (affinelyIf_mono imp_elim_l)).trans <|
    imp_mono h1.1 h2.1

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

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

class IsSplitFraction (α : Type _) [Fraction α] where
  split : α → α × α
  split_add {a : α} : (split a).1 + (split a).2 = a

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

Bool in Init.Prelude

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

Dist in Mathlib.Topology.MetricSpace.Pseudo.Defs

Option.le in Init.Data.Option.Basic

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

instance cmraProd : CMRA (α × β) where
  pcore := pcore
  op := op
  ValidN := ValidN
  Valid := Valid
  op_ne {x} :=
    { ne n y z h := dist_prod_ext (Dist.op_r $ dist_fst h) (Dist.op_r $ dist_snd h) }
  pcore_ne {n x y cx} h ph := by admit /- proof elided -/

def Agree.validN (n : Nat) (x : Agree α) : Prop :=
  match x.car with
  | [_] => True
  | _ => ∀ a ∈ x.car, ∀ b ∈ x.car, a ≡{n}≡ b

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)

instance fromPure_pure_sep_true (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 := by admit /- proof elided -/

MonadExcept in Init.Prelude

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)

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)

Lean.MVarId in Lean.Expr

class LeftId (R : Relation α) (i : α) (f : α → α → α) where
  left_id {x : α} : R (f i x) x

def fixpoint [COFE α] [Inhabited α] (f : α → α) [Contractive f] : α :=
  COFE.compl <| Fixpoint.chain f

instance intoWand_wand (p q : Bool) [BI PROP] (P Q P' : PROP) [h : FromAssumption q P P'] :
    IntoWand p q iprop(P' -∗ Q) P Q where
  into_wand := (intuitionisticallyIf_mono <| wand_mono_l h.1).trans intuitionisticallyIf_elim

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

def mapAllM [Monad M] (f : α → M β) : α × α → M (β × β)
  | (x, y) => do return (← f x, ← f y)

instance (priority := default + 10) fromSep_intuitionistically [BI PROP] (P Q1 Q2 : PROP)
    [h : FromSep P Q1 Q2] : FromSep iprop(□ P) iprop(□ Q1) iprop(□ Q2) where
  from_sep := intuitionistically_sep_2.trans (intuitionistically_mono h.1)

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

def laterChain [OFE A] (c : Chain (Later A)) : Chain A where
  chain n := (c (Nat.succ n)).car
  cauchy Hle := c.cauchy (Nat.succ_le_succ Hle) _ (Nat.lt_succ_self _)

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

def AsEmpValid1.to2 {φ : Prop} {PROP : Type _} {P : PROP} [BI PROP]
    [AsEmpValid1 φ P] : AsEmpValid2 φ P := ⟨AsEmpValid1.as_emp_valid⟩

instance (priority := default + 10) biaffine_absorbing [BI PROP] [BIAffine PROP]
    (P : PROP) : Absorbing P where
  absorbing := (sep_mono_l affine).trans emp_sep.1

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

Coe in Init.Coe

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

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

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

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

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⟩

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

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

instance [BI PROP] : Idempotent (α := PROP) BiEntails or := ⟨or_self⟩

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

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 : 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 BIFUpdatePlainly (PROP MASK : Type _) [BI PROP] [BIFUpdate PROP MASK] [BIPlainly PROP] where
  fupd_plainly_keep_l (E E' : Set MASK) (P R : PROP) : (R ={E,E'}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R
  fupd_plainly_later (E : Set MASK) (P : PROP) : (▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P
  fupd_plainly_sForall_2 (E : Set MASK) (Φ : PROP → Prop) :
    (∀ p, ⌜Φ p⌝ → |={E}=> ■ p) ⊢ |={E}=> sForall Φ

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

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 [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 pureAbsorbing (φ : Prop) [BI PROP] : Absorbing (PROP := PROP) iprop(⌜φ⌝) where
  absorbing := absorbingly_pure.1

instance intoAnd_pure (p : Bool) (φ ψ : Prop) [BI PROP] :
    IntoAnd (PROP := PROP) p iprop(⌜φ ∧ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝) where
  into_and := intuitionisticallyIf_mono pure_and.2

instance (priority := default + 20) fromAssumption_affinely_l (p : Bool) [BI PROP] (P Q : PROP)
    [h : FromAssumption p P Q] : FromAssumption p iprop(<affine> P) Q where
  from_assumption := (intuitionisticallyIf_mono affinely_elim).trans h.1

instance [t : T] : TCOr T U := @TCOr.l T U t

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

class BIUpdateFUpdate (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP MASK] where
  fupd_of_bupd {P : PROP} {E : Set MASK} : iprop(⊢ |==> P) → iprop(⊢ |={E}=> P)

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

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

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

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

instance intoEmpValid_equiv [BI PROP] (P Q : PROP) : IntoEmpValid (P ⊣⊢ Q) iprop(P ∗-∗ Q) where
  into_emp_valid := equiv_wandIff

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

instance intoWand_intuitionistically_wand (p : Bool) [BI PROP] (P Q : PROP) :
    IntoWand p true iprop(□ P -∗ Q) P Q where
  into_wand := intuitionisticallyIf_elim

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 (Fix F) := inferInstanceAs (COFE (Tower F))

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

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

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)

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

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

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

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

instance (priority := default + 10) intoAbsorbingly_intuitionistically [BI PROP] (P : PROP) :
    IntoAbsorbingly iprop(<pers> P) iprop(□ P) where
  into_absorbingly := absorbingly_intuitionistically.2

def iPoseCore {prop : Q(Type u)} (bi : Q(BI $prop)) (val : Expr) (terms : List Term)
    (goals : IO.Ref (Array MVarId)) : TacticM (Q($prop) × Expr) := do
  let hyp ← mkFreshExprMVarQ q($prop)
  let (v, p) ← handleDependentArrows bi val goals
  if let some _ ← try? <| synthInstanceQ q(IntoEmpValid $p $hyp) then
    return ← instantiateForalls bi hyp v terms
  else
    throwError "ipose: {val} is not an entailment"

instance (priority := default + 10) asEmpValidEmpValid2
    [BI PROP] (P : PROP) : AsEmpValid2 (⊢ P) P := AsEmpValid1.to2

k in QqTest.matching

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

@[simp] instance [NumericFraction T] : One (Frac T) := ⟨⟨One.one⟩⟩

abbrev IProp := UPred (IResUR FF)

@[simp] def pcore (s : T) : Option T := some <| hmap (fun _ => CMRA.pcore) s

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

instance intoExists_exists [BI PROP] (Φ : α → PROP) : IntoExists (BI.exists Φ) Φ := ⟨.rfl⟩

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

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 - 20) fromSep_and [BI PROP] (P1 P2 : PROP)
    [TCOr (Affine P1) (Absorbing P2)] [TCOr (Affine P2) (Absorbing P1)] :
    FromSep iprop(P1 ∧ P2) P1 P2 where
  from_sep := sep_and

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

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

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

abbrev FF0 : GFunctors := #[]

Qq.elabTermEnsuringTypeQ in Qq.MetaM

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

instance {x : Agree α} : CMRA.Cancelable x where
  cancelableN {n y z} hval heq := by admit /- proof elided -/

instance [OFE α] : Trans OFE.Equiv OFE.Equiv (OFE.Equiv : α → α → Prop) where
  trans := Equiv.trans

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

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 (priority := default + 20) intoAbsorbingly_absorbing [BI PROP] (P : PROP) [Absorbing P] :
    IntoAbsorbingly P P where
  into_absorbingly := absorbing_absorbingly.2

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

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

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

instance (priority := default - 10) intoPersistently_persistent [BI PROP] (P : PROP)
    [h : Persistent P] : IntoPersistently false P P where
  into_persistently := h.1

Add.add in Init.Prelude

class Persistent [BI PROP] (P : PROP) where
  persistent : P ⊢ <pers> P

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

instance (priority := default + 100) fromAssumption_exact (p : Bool) [BI PROP] (P : PROP) :
    FromAssumption p P P where
  from_assumption := intuitionisticallyIf_elim

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

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

Or.inr in Init.Prelude

EmptyCollection.emptyCollection in Init.Core

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

Nat in Init.Prelude

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)

class IntoWand [BI PROP] (p q : Bool) (R : PROP) (P Q : outParam PROP) where
  into_wand : □?p R ⊢ □?q P -∗ Q

instance emp_persistent [BI PROP] : Persistent (PROP := PROP) iprop(emp) where
  persistent := persistently_emp_intro

Lean.Meta.saveState in Lean.Meta.Basic

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)

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

def GName := LeibnizO Nat

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

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

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

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

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

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

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

Lean.trace in Lean.Util.Trace

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

Repr in Init.Data.Repr

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 (y : α) : CoreId (core y) := CoreId.of_pcore_eq_some (pcore_eq_core _)

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

instance [u : U] : TCOr T U := @TCOr.r T U u

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

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

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

instance [H : Cancelable (some x)] : Cancelable (point (T := T) i (some x)) where
  cancelableN {n m1 m2} Hv He j := by admit /- proof elided -/

instance [BI PROP] [BIAffine PROP] (P : PROP) : Absorbing P where
  absorbing := (sep_mono_l affine).trans emp_sep.1

instance cmraOption : CMRA (Option α) where
  pcore x := some (optionCore x)
  op := optionOp
  ValidN := optionValidN
  Valid := optionValid
  op_ne.ne n x1 x2 H := by admit /- proof elided -/
</all_available_defs>

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

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 _root_.Iris.OFE.Equiv.op_l {x y z : α} : x ≡ y → x • z ≡ y • z

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

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

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

theorem op_eqv {x x' y y' : α} (ex : x ≡ x') (ey : y ≡ y') : x • y ≡ x' • y'

theorem _root_.Iris.OFE.Equiv.op : (x : α) ≡ x' → y ≡ y' → x • y ≡ x' • y'

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 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 plainly_exists [BIPlainlyExists PROP] {Ψ : α → PROP} : ■ (∃ a, Ψ a) ⊣⊢ ∃ a, ■ (Ψ a)

theorem hmap_unalloc [Heap T K V] {t : T} (H : get t k = none) : get (hmap f t) k = none

theorem LocalUpdate.delete_option (x : Option α) (y : α) [CMRA.Exclusive y] :
    (x, some y) ~l~> (none, none)

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

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

theorem affinely_and [BI PROP] {P Q : PROP} : <affine> (P ∧ Q) ⊣⊢ <affine> P ∧ <affine> Q

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem assoc_L {x y z : α} : x • (y • z) = (x • y) • z

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

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

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

theorem intuitionisticallyIf_exists {p : Bool} [BI PROP] {Ψ : α → PROP} :
    (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a

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 LocalUpdate.cancel (x y z : α) [CMRA.Cancelable x] : (x • y, x • z) ~l~> (y, z)

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

theorem Update.op {x₁ x₂ y₁ y₂ : α} (xy₁ : x₁ ~~> y₁) (xy₂ : x₂ ~~> y₂) : x₁ • x₂ ~~> y₁ • y₂

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

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

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

theorem Frac.inc_iff_lt {p q : Frac α} : p ≼ q ↔ p < q

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

theorem sep_emp_intro_intuitionistic [BI PROP] {P Q : PROP}
    (h : P ⊢ Q) : P ∗ □ emp ⊢ Q

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

theorem plainly_and_sep_l_1 : ■ P ∧ Q ⊢ ■ P ∗ Q

theorem _root_.Iris.OFE.Equiv.valid : (x : α) ≡ y → (✓ x ↔ ✓ y)

theorem equivalence_eq : Equivalence (@Eq α)

theorem valid_core {x : α} (v : ✓ x) : ✓ core x

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

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 and [BI PROP] (Q : PROP) : Q ⊢ Q ∧ Q

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

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

theorem persistentlyIf_pure {p : Bool} [BI PROP] {φ : Prop} : (<pers>?p ⌜φ⌝ : PROP) ⊣⊢ ⌜φ⌝

theorem bupd_except0 {P : PROP} : iprop(◇ (|==> P) ⊢ (|==> ◇ P))

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

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

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

theorem lt_trans {a b c : α} : a < b → b < c → a < c

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

theorem bigOp_sep_cons [BI PROP] {P : PROP} {Ps : List PROP} :
    [∗] (P :: Ps) ⊣⊢ P ∗ [∗] Ps

theorem Agree.op_assoc {x y z : Agree α} :  x.op (y.op z) ≡ (x.op y).op z

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

theorem rec_apply [BI PROP] {P Q P' Q' Q1 Q2 R : PROP}
    (h1 : P ⊣⊢ P' ∗ Q') (h2 : Q' ⊢ Q1) (h3 : P' ∗ Q2 ⊢ R)
    [IntoWand false false Q Q1 Q2] : P ∗ Q ⊢ R

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

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

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

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

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 split_es [BI PROP] {Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : emp ∗ Q ⊣⊢ Q1 ∗ Q2

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

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

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

theorem and_clear_intuitionistic_multiple [BI PROP] (Q : PROP) : □ (P1 ∧ P2 ∧ Q ∧ P3) ⊢ Q

theorem intuitionisticallyIf_def' {p : Bool} [BI PROP] {P : PROP} :
    iprop(□?p P) = iprop(<affine>?p <pers>?p P)

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

theorem empty_disjoint {s : State Val} : ∅ |

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

theorem intuitionisticallyIf_emp {p : Bool} [BI PROP] : (□?p emp : PROP) ⊣⊢ emp

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

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

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

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

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

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

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

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

theorem intuitionistically_elim_emp [BI PROP] {P : PROP} : □ P ⊢ emp

theorem intuitionistically_of_intuitionistic [BI PROP] {P : PROP} [Affine P] [Persistent P] :
    □ P ⊣⊢ P

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

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

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

theorem pure_assumption [BI PROP] {P A Q : PROP} (h_P : ⊢ A)
    [inst : FromAssumption true A Q] [TCOr (Affine P) (Absorbing Q)] :
    P ⊢ Q

theorem _root_.Iris.OFE.Equiv.cancelable {x₁ x₂ : α} : x₁ ≡ x₂ → (Cancelable x₁ ↔ Cancelable x₂)

theorem intuitionistically_and [BI PROP] {P Q : PROP} : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q

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

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

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

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

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

theorem discrete_inc_l {x y : α} [HD : DiscreteE x] (Hv : ✓{0} y) (Hle : x ≼{0} y) : x ≼ y

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

theorem Discrete.discrete_n [OFE α] [Discrete α] {n} {x y : α} (h : x ≡{0}≡ y) : x ≡{n}≡ y

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 and_true [BI PROP] {P : PROP} : P ∧ True ⊣⊢ P

theorem conv_compl' [COFE α] {c : Chain α} {n i} (h : n ≤ i) : compl c ≡{n}≡ c i

theorem split_se [BI PROP] {P P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ emp ⊣⊢ P1 ∗ P2

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

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

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

theorem valid_own_op {dq : DFrac F} {q : F} : ✓ own q • dq → Fractional q

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

theorem false_elim_spatial [BI PROP] {P Q : PROP} : P ∗ False ⊢ Q

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

theorem plainly_or [BIPlainlyExists PROP] : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q

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

theorem «forall» [BI PROP] : ⊢ ∀ x, ⌜x = 0⌝ → (⌜x = 0⌝ : PROP)

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

theorem op_opM_assoc (x y : α) (mz : Option α) : (x • y) •? mz ≡ x • (y •? mz)

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

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

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

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

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

theorem unit_right_id {x : α} : x • unit ≡ x

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

theorem or [BI PROP] : ⊢ True ∨ (False : PROP)

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

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

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

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

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

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

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

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

theorem plainly_and_sep_assoc : ■ P ∧ (Q ∗ R) ⊣⊢ (■ P ∧ Q) ∗ R

theorem le_rfl {a : α} : a ≤ a

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

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

theorem affinelyIf_emp {p : Bool} [BI PROP] : (<affine>?p emp : PROP) ⊣⊢ emp

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

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

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

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

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

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

theorem persistently_forall_1 [BI PROP] {Ψ : α → PROP} : <pers> (∀ a, Ψ a) ⊢ ∀ a, <pers> (Ψ a)

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

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

theorem DFrac.update_discard {dq : DFrac F} : dq ~~> .discard

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

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

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

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

theorem incN_refl (x : α) : x ≼{n} x

theorem later_and [BI PROP] {P Q : PROP} : ▷ (P ∧ Q) ⊣⊢ ▷ P ∧ ▷ Q

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

theorem plainly_elim [Absorbing P] : ■ P ⊢ P

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

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

theorem lean [BI PROP] (Q : PROP) (H : ⊢ Q) : <affine> P ⊢ Q

theorem Update.option (x y : α) (uxy : x ~~> y) : some x ~~> some y

theorem down_up : ∀ {k} x, down F k (up F k x) ≡ x

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

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

@[rw_mono_rule]
theorem affinely_mono [BI PROP] {P Q : PROP} : (P ⊢ Q) → <affine> P ⊢ <affine> Q

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

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

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

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

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

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

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

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

theorem simple [BI PROP] : ⊢ (⌜True⌝ : PROP)

theorem pure_true [BI PROP] {φ : Prop} (h : φ) : ⌜φ⌝ ⊣⊢ (True : PROP)

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 set_op_eq [IsoFunStore T K (Option V)] {m1 m2 : T} :
    (set (V := Option V) (m1 • m2) i (x • y)) = (set m1 i x • set m2 i y)

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

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

theorem absorbingly_affinely_intro_of_persistent [BI PROP] {P : PROP} [Persistent P] :
    P ⊢ <absorb> <affine> P

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

theorem or_elim_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [IntoOr A A1 A2]
    (h1 : P ∗ □ A1 ⊢ Q) (h2 : P ∗ □ A2 ⊢ Q) : P ∗ □ A ⊢ Q

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

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

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

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

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

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

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

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

theorem Agree.dist_def {x y : Agree α} : x ≡{n}≡ y ↔ Agree.dist n x y

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

theorem split_sr [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ P1 ∗ (P2 ∗ Q)

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

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

theorem unit_left_id_L {x : α} : unit • x = x

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

<local_ctx>
import Iris.Algebra.CMRA

import Iris.Algebra.OFE

namespace Iris

section agree

variable {α : Type u}

variable (α) in

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

variable [OFE α]

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)

def Agree.validN (n : Nat) (x : Agree α) : Prop :=
  match x.car with
  | [_] => True
  | _ => ∀ a ∈ x.car, ∀ b ∈ x.car, a ≡{n}≡ b

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

<target_theorem>
theorem Agree.op_inv {x y : Agree α} : (x.op y).valid → x ≡ y :=
</target_theorem>

