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)

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

@[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 Hom (α β : Type _) [OFE α] [OFE β] where
  f : α → β
  ne : NonExpansive f

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

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

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

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

local instance : IsGFunctors FF0 := nofun

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

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

Lean.Elab.Tactic.withoutRecover in Lean.Elab.Tactic.Basic

def isplitCore (side : splitSide) (names : Array (TSyntax `ident)) : TacticM Unit := do
  let splitRight := match side with
    | .splitLeft => false
    | .splitRight => true

LT in Init.Prelude

abbrev FF0 : GFunctors := #[]

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

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

HasSubset in Init.Core

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

instance unit_CoreId : CoreId (unit : α) where
  core_id := pcore_unit

Nat.le_or_ge in Init.Data.Nat.Basic

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

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

instance [OFE α] [OFE β] : CoeFun (α -c> β) (fun _ => α → β) := ⟨fun x => x.toHom.f⟩

instance intoPure_exists [BI PROP] (Φ : α → PROP) (φ : α → Prop)
    [h : ∀ x, IntoPure (Φ x) (φ x)] : IntoPure iprop(∃ x, Φ x) (∃ x, φ x) where
  into_pure := (exists_mono fun x => (h x).1).trans pure_exists.1

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

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

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

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

instance later_persistent [BI PROP] {P : PROP} [Persistent P] : Persistent iprop(▷ P) where
  persistent := (later_mono persistently_intro).trans later_persistently.mp

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

instance urFunctorContractiveOptionOF
    [RFunctorContractive F] : URFunctorContractive (OptionOF F) where
  map_contractive.1 := COFE.OFunctorContractive.map_contractive.1

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

instance exclusive_cancelable {x : α} [Exclusive x] : Cancelable x where
  cancelableN v _ := absurd v not_valid_exclN_op_left

Qq.instantiateMVarsQ in Qq.MetaM

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

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 bigSep [BIBase PROP] (Ps : List PROP) : PROP := bigOp sep iprop(emp) Ps

instance isCOFE_later [OFE A] [IsCOFE A] : IsCOFE (Later A) where
  compl c := Later.next (IsCOFE.compl (laterChain c))
  conv_compl {n} c := by admit /- proof elided -/

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

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 Replaces [BI PROP] (K A B : PROP) := (B -∗ K) ⊢ (A -∗ K)

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

def SpecializeState.process1 :
    @SpecializeState u prop bi orig → Term → TermElabM (SpecializeState bi orig)
  | { e, hyps, b, out, pf }, arg => do
    let uniq ← match arg with
      | `($x:ident) => try? (hyps.findWithInfo x)
      | _ => pure none
    if let some uniq := uniq then
      
      let ⟨e', hyps', out₁, out₁', b1, _, pf'⟩ := hyps.remove false uniq
      let b2 := if b1.constName! == ``true then b else q(false)
      have : $out₁ =Q iprop(□?$b1 $out₁') := ⟨⟩
      have : $b2 =Q ($b1 && $b) := ⟨⟩

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 or_persistent [BI PROP] (P Q : PROP) [Persistent P] [Persistent Q] :
    Persistent iprop(P ∨ Q) where
  persistent := (or_mono persistent persistent).trans persistently_or.2

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

def Heap.point [Heap T K V] (k : K) (v : Option V) : T := set empty k v

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

instance 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

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

def A' : Nat → Σ α : Type u, COFE α
  | 0 => ⟨ULift Unit, inferInstance⟩
  | n+1 => let ⟨A, _⟩ := A' n; ⟨F A A, inferInstance⟩

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

Inhabited.default in Init.Prelude

EmptyCollection in Init.Core

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

Lean.Expr in Lean.Expr

def laterMap [OFE A] [OFE B] (f : A -n> B)  : Later A -n> Later B :=

for goal in goals do
        match rule? with
        | some rule =>
          if ← go goal rule then
            rule? := none
        | none =>
          applyReflexivity goal

def Frac (α : Type _) := LeibnizO α

inductive iCasesPat
  | one (name : TSyntax ``binderIdent)
  | clear
  | conjunction (args : List iCasesPat)
  | disjunction (args : List iCasesPat)
  | pure           (pat : iCasesPat)
  | intuitionistic (pat : iCasesPat)
  | spatial        (pat : iCasesPat)
  deriving Repr, Inhabited

| .conjunction (arg :: args) => do
    let exres ← try? (α := _ × (v : Level) × (α : Q(Sort v)) × (Φ : Q($α → $prop)) ×
        Q(IntoExists $A' $Φ)) do
      let .one n := arg | failure
      let v ← mkFreshLevelMVar
      let α ← mkFreshExprMVarQ q(Sort v)
      let Φ ← mkFreshExprMVarQ q($α → $prop)
      Pure.pure ⟨n, v, α, Φ, ← synthInstanceQ q(IntoExists $A' $Φ)⟩
    if let some ⟨n, _, α, Φ, inst⟩ := exres then
      iCasesExists bi P Q A' p n α Φ inst
        (iCasesCore hyps Q p · · · (.conjunction args) k)
    else
      let A1 ← mkFreshExprMVarQ q($prop)
      let A2 ← mkFreshExprMVarQ q($prop)
      let inst ← try? (α := Q(IntoAnd $p $A' $A1 $A2)) do
        unless arg matches .clear || args matches [.clear] || p.constName! == ``true do failure
        synthInstanceQ q(IntoAnd $p $A' $A1 $A2)
      if let (.clear, some inst) := (arg, inst) then
        iCasesAndLR bi P Q A' A1 A2 p inst (right := true) fun B B' h =>
          iCasesCore hyps Q p B B' h (.conjunction args) @k
      else if let ([.clear], some inst) := (args, inst) then
        iCasesAndLR bi P Q A' A1 A2 p inst (right := false) fun B B' h =>
          iCasesCore hyps Q p B B' h arg @k
      else
        iCasesSep bi hyps Q A' A1 A2 p inst @k
          (iCasesCore · · p · · · arg)
          (iCasesCore · · p · · · (.conjunction args))

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

class Plain [BI PROP] [Plainly PROP] [BIPlainly PROP] (P : PROP) where
  plain : P ⊢ ■ P

def IrisGoal.strip : IrisGoal → Expr
  | { e, goal, .. } => q(Entails $e $goal)

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

class IsoFunStore (T : Type _) (K V : outParam (Type _)) [Store T K V] extends RepFunStore T K V where
  of_fun_get {t : T} : of_fun ⟨get t, rep_get t⟩ = t

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

class FromPure [BI PROP] (a : outParam Bool) (P : PROP) (φ : outParam Prop) where
  from_pure : <affine>?a ⌜φ⌝ ⊢ P

instance : COFE (iPrePropO FF) := inferInstanceAs (COFE (OFunctor.Fix _))

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

def Disjoint (x y : Set α) : Prop := ∀ a, ¬(x a ∧ y a)

def Fix.iso : OFE.Iso (F (Fix F) (Fix F)) (Fix F) := Tower.iso

instance intoExists_pure (φ : α → Prop) [BI PROP] :
    IntoExists (PROP := PROP) iprop(⌜∃ x, φ x⌝) (fun a => iprop(⌜φ a⌝)) where
  into_exists := pure_exists.2

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

instance fromOr_or [BI PROP] (P1 P2 : PROP) : FromOr iprop(P1 ∨ P2) P1 P2 := ⟨.rfl⟩

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 RFunctorContractive.toOFunctorContractive
    [RFunctorContractive F] : COFE.OFunctorContractive F where
  map_contractive.1 := map_contractive.1

Lean.Macro.throwUnsupported in Init.Prelude

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

def mkIntuitionisticIf {prop : Q(Type u)} (_bi : Q(BI $prop))
    (p : Q(Bool)) (e : Q($prop)) : {A : Q($prop) // $A =Q iprop(□?$p $e)} :=
  match matchBool p with
  | .inl _ => ⟨q(iprop(□ $e)), ⟨⟩⟩
  | .inr _ => ⟨e, ⟨⟩⟩

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

outParam in Init.Prelude

Lean.MacroM in Init.Prelude

instance fromAffinely_affine [BI PROP] (P : PROP) [Affine P] : FromAffinely P P true where
  from_affinely := affinely_elim

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

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

def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop))
    {P} (hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool))
    (k : ∀ {P}, Hyps bi P → MetaM Q($P ⊢ $Q)) :
    MetaM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
  try
    let ⟨_⟩ ← assertDefEqQ A' q(iprop(False))
    if p.constName! == ``true then
      have : $p =Q true := ⟨⟩; return q(false_elim_intuitionistic)
    else
      have : $p =Q false := ⟨⟩; return q(false_elim_spatial)
  catch _ =>
    let ⟨_⟩ ← assertDefEqQ A' q(iprop(emp))
    if p.constName! == ``true then
      have : $p =Q true := ⟨⟩; return q(sep_emp_intro_intuitionistic $(← k hyps))
    else
      have : $p =Q false := ⟨⟩; return q(sep_emp_intro_spatial $(← k hyps))

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

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

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

instance fromImp_imp [BI PROP] (P1 P2 : PROP) : FromImp iprop(P1 → P2) P1 P2 := ⟨.rfl⟩

def mapCodHom [OFEFun (β₁ : α → _)] [OFEFun β₂]
    (F : ∀ x, β₁ x -n> β₂ x) : ((x : α) → β₁ x) -n> ((x : α) → β₂ x) where
  f f x := F x (f x)
  ne.1 _ _ _ H x := (F x).ne.1 (H x)

Lean.MVarId in Lean.Expr

@[match_pattern] def nameAnnotation := `name

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

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

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

class IntoPure [BI PROP] (P : PROP) (φ : outParam Prop) where
  into_pure : P ⊢ ⌜φ⌝

Nat.eq_or_lt_of_le in Init.Prelude

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

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

instance sep_affine [BI PROP] (P Q : PROP) [Affine P] [Affine Q] : Affine iprop(P ∗ Q) where
  affine := (sep_mono affine affine).trans sep_emp.1

@[delab app.Iris.ProofMode.Entails']
def delabIrisGoal : Delab := do
  let expr ← instantiateMVars <| ← getExpr

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

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

instance : OFE Unit where
  Equiv _ _ := True
  Dist _ _ _ := True
  dist_eqv := ⟨fun _ => ⟨⟩, id, fun _ => id⟩
  equiv_dist := 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

def Union {X : Type _} (S1 S2 : X → Prop) : X → Prop :=
  fun x => S1 x ∨ S2 x

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

instance [OFE α] [OFE β] (f : α -n> β) : NonExpansive f := f.ne

Qq.withLocalDeclDQ in Qq.MetaM

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

protected def and (P Q : UPred M) : UPred M where
  holds n x := P n x ∧ Q n x
  mono HPQ Hle Hn := ⟨P.mono HPQ.1 Hle Hn, Q.mono HPQ.2 Hle Hn⟩

instance intoAnd_affinely (p : Bool) [BI PROP] (P Q1 Q2 : PROP) [h : IntoAnd p P Q1 Q2] :
    IntoAnd p iprop(<affine> P) iprop(<affine> Q1) iprop(<affine> Q2) where
  into_and := intuitionisticallyIf_affinely.1.trans <| (affinely_mono h.1).trans <|
    intuitionisticallyIf_affinely.2.trans (intuitionisticallyIf_mono affinely_and.1)

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

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

instance [OFE α] {n : Nat} : Trans (OFE.Dist n) (OFE.Dist n) (OFE.Dist n : α → α → Prop) where
  trans := Dist.trans

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

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

instance : Leibniz (Frac α) := inferInstanceAs (Leibniz (LeibnizO α))

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

@[simp] def validN (n : Nat) (s : T) : Prop := ∀ k, ✓{n} (get s k : Option V)

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

Pure in Init.Prelude

abbrev IResF (FF : GFunctors) : COFE.OFunctorPre :=
  DiscreteFunOF (fun i : GId FF => GenMapOF GName FF[i])

instance [Fraction α] {a : Frac α} : CMRA.IdFree a where
  id_free0_r b _ H := by admit /- proof elided -/

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

instance : HasSubset (State Val) where
  Subset a b := ∀ i x, a i = result x → b i = result x

instance [BI PROP] : Commutative (α := PROP) BiEntails or := ⟨or_comm⟩

def «forall» [BIBase PROP] {α : Sort _} (P : α → PROP) : PROP := sForall fun p => ∃ a, P a = p

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

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⟩

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)

instance uPred_entails_preorder : Std.Preorder (Entails (PROP := UPred M)) where
  refl _ _ _ H := H
  trans H1 H2 _ _ Hv H := H2 _ _ Hv <| H1 _ _ Hv H

Lean.Meta.saveState in Lean.Meta.Basic

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

def maps_to (l : Nat) (v : Val) : HeapProp Val :=
  fun state => state l = result v

Lean.mkIdent in Init.Meta.Defs

class IntoForall [BI PROP] (P : PROP) {α : outParam (Sort _)} (Φ : outParam <| α → PROP) where
  into_forall : P ⊢ ∀ x, Φ x

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

| .disjunction [] => throwUnsupportedSyntax
</all_available_defs>

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

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

theorem valid_mapN {x y : α} (f : ∀ n, ✓{n} x → ✓{n} y) (v : ✓ x) : ✓ y

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

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 valid_of_eqv {x y : α} : x ≡ y → ✓ x → ✓ y

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

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

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

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

theorem plainly_cmra_cmraValid_1 [CMRA A] (a : A) :
    (cmraValid a : UPred M) ⊢ ■ cmraValid a

theorem op_monoN_left {n x y} (z : α) (h : x ≼{n} y) : x • z ≼{n} y • z

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

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

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

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

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

theorem distLater_succ [OFE α] {n} {x y : α} : DistLater n.succ x y ↔ x ≡{n}≡ y

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

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

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

theorem disjoint_comm {a b : State Val} : a |

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

theorem Equiv.of_eq [OFE α] {x y : α} : x = y → x ≡ y

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

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

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

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

theorem incN_unit {n} {x : α} : unit ≼{n} x

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

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

theorem loeb_weak_of_strong [BI PROP] {P : PROP} (H : ∀ P : PROP, (▷ P → P) ⊢ P)
    (H' : ▷ P ⊢ P) : True ⊢ P

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

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

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

theorem exact_forall [BI PROP] (P : α → PROP) (a : α) (H : ⊢ ∀ x, P x) : ⊢ P a

theorem later_affinely [BI PROP] [BIAffine PROP] {P : PROP} : <affine> ▷ P ⊣⊢ ▷ <affine> P

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

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

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

theorem bupd_idem {P : PROP} : iprop((|==> |==> P) ⊣⊢ |==> P)

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

theorem later_true [BI PROP] : (▷ True ⊣⊢ (True : PROP))

theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} {Φ : α → PROP}
    [inst : IntoForall P Φ] (h : A1 ⊢ A2 ∗ □?p P) (a : α) : A1 ⊢ A2 ∗ □?p (Φ a)

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

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

theorem plainly_affinely_elim : ■ <affine> P ⊣⊢ ■ P

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

@[simp] theorem map_id [OFE α] {c : Chain α} : map (Hom.id : α -n> α) c = c

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

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

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

theorem cmraValid_elim [CMRA A] (a : A) : (cmraValid a : UPred M) ⊢ iprop(⌜ ✓{0} a ⌝)

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

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

theorem add_le_mono {a b c : α} : a + b ≤ c → a ≤ c

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

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

theorem excl_map_compose (f : α → β) (g : β → γ) :
    map (g ∘ f) x = map g (map f x)

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

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

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

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

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

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

@[simp] theorem Contractive.zero [OFE α] [OFE β] (f : α → β) [Contractive f] {x y} :
    f x ≡{0}≡ f y

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Dist.le [OFE α] {m n} {x y : α} (h : x ≡{n}≡ y) (h' : m ≤ n) : x ≡{m}≡ y

theorem plainly_elim [Absorbing P] : ■ P ⊢ P

theorem LocalUpdate.total_valid0 [CMRA.IsTotal α] {x y x' y' : α}
    (h : ✓{0} x → ✓{0} y → y ≼{0} x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y')

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Replaces.apply [BI PROP] {P P' Q : PROP}
    (h : Replaces Q P P') (h_entails : P' ⊢ Q) : P ⊢ Q

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

theorem intuitionistically_or [BI PROP] {P Q : PROP} : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q

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

theorem absorbing_of_emp_absorbing [BI PROP] [Absorbing (emp : PROP)] (P : PROP) : Absorbing P

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

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

theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP}
    [FromImp Q A1 A2] [inst : FromAffinely B A1] [or : TCOr (Persistent A1) (Intuitionistic P)]
    (h : P ∗ B ⊢ A2) : P ⊢ Q

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

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

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

theorem entails_impl_true [BI PROP] {P Q : PROP} :
    (P ⊢ Q) ↔ iprop((True : PROP) ⊢ (P → Q))

theorem validN_op_unit {n} {x : Option α} (vx : ✓{n} x) : ✓{n} x • unit

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

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

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

theorem or_false [BI PROP] {P : PROP} : P ∨ False ⊣⊢ P

theorem bupd_and {P Q : PROP} : iprop((|==> (P ∧ Q)) ⊢ (|==> P) ∧ (|==> Q))

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

theorem dom_op_union (m1 m2 : T) : dom (m1 • m2) = Set.Union (dom m1) (dom m2)

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

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

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

theorem LocalUpdate.prod_2 (x1 y1 : α) {x2 y2 x2' y2' : β}
    (h : (x2, y2) ~l~> (x2', y2')) : ((x1, x2), (y1, y2)) ~l~> ((x1, x2'), (y1, y2'))

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

theorem valid_opM {x : α} {my : Option α} : ✓ (x •? my) → ✓ x

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

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

theorem point_op_point_eq [IsoFunStore T K (Option V)] {i : K} {x y : V} :
    (point (T := T) i (some x)) • (point i (some y)) = (point i (some (x • y)))

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

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

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

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

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

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

theorem prod.is_discrete [OFE α] [OFE β] {a : α} {b : β} (Ha : DiscreteE a) (Hb : DiscreteE b) :
    DiscreteE (a, b)

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

theorem bigOp_nil {f : PROP → PROP → PROP} {unit : PROP} : bigOp f unit [] = unit

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

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

theorem with_proof [BI PROP] (H : A → B) (P Q : PROP) : <affine> P ⊢ <pers> Q → ⌜A⌝ → ⌜B⌝

protected theorem Tower.up (X : Tower F) : up F (k+1) (X (k+1)) ≡{k}≡ X (k+2)

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

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

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

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

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

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

theorem LimitPreserving.equiv [COFE α] [COFE β] (f g : α -n> β) :
    LimitPreserving (fun x => f x ≡ g x)

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

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

theorem Update.exclusive {x y : α} [CMRA.Exclusive x] (vy : ✓ y) : x ~~> y

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 forall_spatial [BI PROP] (Q : Nat → PROP) : ⊢ (∀ x, Q x) -∗ Q (y + 1)

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

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

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

theorem pcore_mono {x y : α} : x ≼ y → pcore x = some cx → ∃ cy, pcore y = some cy ∧ cx ≼ cy

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

theorem true_emp [BI PROP] [h : BIAffine PROP] : (True : PROP) ⊣⊢ emp

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

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

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

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

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

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

theorem disjoint_op_eq_union [IsoFunStore T K (Option V)] {m1 m2 : T} (H : Set.Disjoint (dom m1) (dom m2)) :
    m1 • m2 = Heap.union m1 m2

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

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

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

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

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

theorem op_core_dist (x : α) : x • core x ≡{n}≡ x

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem pure_forall_2 [BI PROP] {φ : α → Prop} : ⌜∀ x, φ x⌝ ⊢ ∀ x, (⌜φ x⌝ : PROP)

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

theorem assoc_L {x y z : α} : x • (y • z) = (x • y) • z
</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 ≠ []

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

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.valid (x : Agree α) : Prop := ∀ n, x.validN n
</local_ctx>

<target_theorem>
theorem Agree.toAgree_uninj {x : Agree α} : ✓ x → ∃ a, toAgree a ≡ x :=
</target_theorem>

