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

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

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

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

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

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

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

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

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

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

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

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

open Set
open Mathlib
open SetRel

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

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

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

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

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

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

@[simp]
</local_ctx>

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

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

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

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

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

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

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

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

### Your task:
<all_available_defs>
class 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

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

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

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

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

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

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

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

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

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

instance intuitionistically_intuitionistic [BI PROP] (P : PROP) : Intuitionistic iprop(□ P) where
  intuitionistic := intuitionistically_idem.2

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

@[simp] instance : COFE (Frac α) := inferInstanceAs (COFE (LeibnizO α))

Nat.le_or_ge in Init.Data.Nat.Basic

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

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

| .clear => do
    let pf ← clearCore bi q(iprop($P ∗ $A)) P A Q q(.rfl)
    pure q($pf $(← k hyps))

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

Qq.instantiateMVarsQ in Qq.MetaM

structure Later (A : Type u) : Type (u+1) where
  next :: car : A

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

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 {F} [COFE.OFunctor F] : RFunctor (ExclOF F) where
  cmra := inferInstance
  map f g := exclO_map (COFE.OFunctor.map f g)
  map_ne.ne := by admit /- proof elided -/

instance sep_intuitionistic [BI PROP] (P Q : PROP) [Intuitionistic P] [Intuitionistic Q] :
    Intuitionistic iprop(P ∗ Q) where
  intuitionistic := (sep_mono intuitionistic intuitionistic).trans intuitionistically_sep_2

instance {f : F} : CMRA.IdFree (own f) where
  id_free0_r := by admit /- proof elided -/

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

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

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

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

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

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

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

Unit in Init.Prelude

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

inductive SplitResult {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where
  | emp (_ : $e =Q BI.emp)
  | left
  | right
  | split {elhs erhs : Q($prop)} (lhs : Hyps bi elhs) (rhs : Hyps bi erhs)
          (pf : Q($e ⊣⊢ $elhs ∗ $erhs))

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

class FromSep [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
  from_sep : Q1 ∗ Q2 ⊢ P

class IntoEmpValid (φ : Prop) {PROP : outParam (Type _)} (P : outParam PROP) [BI PROP] where
  into_emp_valid : φ → ⊢ P

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

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

instance [OFE α] [IsCOFE α] : IsCOFE (Excl α) where
  compl c := (c 0).map fun x => IsCOFE.compl (exclChain c x)
  conv_compl {n} c := by admit /- proof elided -/

Lean.LocalContext in Lean.LocalContext

op_ne := Agree.op_ne
  pcore_ne := by admit /- proof elided -/

structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where
  (e : Q($prop)) (hyps : Hyps bi e) (b : Q(Bool)) (out : Q($prop))
  pf : Q($orig ⊢ $e ∗ □?$b $out)

nonrec abbrev OFE.ContractiveHom.fixpoint [COFE α] [Inhabited α] (f : α -c> α) : α := fixpoint f.f

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

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

Union in Init.Core

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

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 Φ

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 intoAnd_persistently (p : Bool) [BI PROP] (P Q1 Q2 : PROP) [h : IntoAnd p P Q1 Q2] :
    IntoAnd p iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2) where
  into_and := by admit /- proof elided -/

Equivalence in Init.Core

applyMonotonicity (goal : MVarId) : TacticM <| Option <| List MVarId := do
    for rule in (← getMonotonicityRules) do
      try
        if let some goals ← apply' goal rule then
          return ← goals.mapM normalizeGoal
      catch _ =>
        continue
    return none

instance DiscreteFunOF_URFC {C} (F : C → COFE.OFunctorPre) [HURF : ∀ c, URFunctorContractive (F c)] :
    URFunctorContractive (DiscreteFunOF F) where
  map_contractive.1 h _ _ := URFunctorContractive.map_contractive.distLater_dist h _

instance ucmraOption : UCMRA (Option α) where
  unit := none
  unit_valid := by admit /- proof elided -/

Lean.Expr.fvar in Lean.Expr

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

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

instance (priority := default + 30) fromAssumption_persistently_l_false [BI PROP] [BIAffine PROP]
    (P Q : PROP) [h : FromAssumption true P Q] : FromAssumption false iprop(<pers> P) Q where
  from_assumption := intuitionistically_iff_persistently.2.trans h.1

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

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

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 [OFEFun (β : α → _)] : OFE ((x : α) → β x) where
  Equiv f g := ∀ x, f x ≡ g x
  Dist n f g := ∀ x, f x ≡{n}≡ g x
  dist_eqv := {
    refl _ _ := dist_eqv.refl _
    symm h _ := dist_eqv.symm (h _)
    trans h1 h2 _ := dist_eqv.trans (h1 _) (h2 _)
  }
  equiv_dist {_ _} := by admit /- proof elided -/

class BILaterContractive (PROP : Type _) [BI PROP] extends OFE.Contractive later (α := PROP)

GetElem in Init.GetElem

@[simp] def Excl.Valid : Excl α → Prop
  | excl _ => True
  | invalid => False

class HasStoreMap (T1 T2 : Type _) (K V1 V2 : outParam (Type _)) [Store T1 K V1] [Store T2 K V2] where
   
  dmap (f : K → V1 → V2) : T1 → T2
  get_dmap : get (dmap f t) k = f k (get t k)

class Leibniz (α : Type _) [OFE α] where
  eq_of_eqv {x y : α} : x ≡ y → x = y

Bool in Init.Prelude

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

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

let goal ← match direction with
    | .forward => do
      goalR.setTag tag
      pure goalL
    | .reverse => do
      goalL.setTag tag
      pure goalR

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

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

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 : BIAffine (UPred M) := ⟨by admit /- proof elided -/
⟩

instance fromExists_affinely [BI PROP] (P : PROP) (Φ : α → PROP) [h : FromExists P Φ] :
    FromExists iprop(<affine> P) (fun a => iprop(<affine> (Φ a))) where
  from_exists := affinely_exists.2.trans <| affinely_mono h.1

let some { hyps, goal, .. } := parseIrisGoal? expr | failure

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

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

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

abbrev constOF (B : Type) : OFunctorPre := fun _ _ _ _ => B

ULift in Init.Prelude

instance [OFE α] [OFE β] (iso : Iso α β) : NonExpansive iso.hom := iso.hom.ne

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

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 [Fraction α] [CMRA α] {a : Frac α} (Hw : Whole a.1) : Exclusive a where
  exclusive0_l _ Hk := (not_exists.mp Hw.2) _ Hk

structure IrisGoal where
  u : Level
  prop : Q(Type u)
  bi : Q(BI $prop)
  e : Q($prop)
  hyps : Hyps bi e
  goal : Q($prop)

instance exists_absorbing [BI PROP] (Φ : α → PROP) [∀ x, Absorbing (Φ x)] :
    Absorbing iprop(∃ x, Φ x) where
  absorbing := absorbingly_exists.1.trans (exists_mono fun _ => absorbing)

instance : BILaterContractive (UPred M) where
  toContractive := later_contractive

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)

def Store.all [Store T K V] (P : K → V → Prop) : T → Prop :=
  fun t => ∀ k, P k (get t k)

protected def persistently (P : UPred M) : UPred M where
  holds n x := P n (CMRA.core x)
  mono H Hx Hn := P.mono H (CMRA.core_incN_core Hx) Hn

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

def findGoalFromTag? (tag : Name) : TacticM <| Option MVarId := do
  (← getUnsolvedGoals).findM? fun goal => do return (← goal.getTag) == tag

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

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

def Tower.iso : OFE.Iso (F (Tower F) (Tower F)) (Tower F) where
  hom.f X := {
    val n := (down F n).comp (map (Tower.embed _) (Tower.proj _)) X
    down {n} := (down ..).ne.eqv <|
      (map_comp ..).symm.trans (map_ne.eqv Tower.embed_up (·.down) _)
  }
  hom.ne.1 _ _ _ h _ := by admit /- proof elided -/

class IdFree (x : α) where
  id_free0_r y : ✓{0} x → ¬x • y ≡{0}≡ x

One in Init.Prelude

instance persistently_persistent [BI PROP] (P : PROP) : Persistent iprop(<pers> P) where
  persistent := persistently_idem_2

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

instance wand_absorbing_r [BI PROP] (P Q : PROP) [Absorbing Q] : Absorbing iprop(P -∗ Q) where
  absorbing := absorbingly_wand_1.trans (wand_mono absorbingly_intro absorbing)

instance intoAnd_intuitionistically (p : Bool) [BI PROP] (P Q1 Q2 : PROP) [h : IntoAnd p P Q1 Q2] :
    IntoAnd p iprop(□ P) iprop(□ Q1) iprop(□ Q2) where
  into_and := (intuitionisticallyIf_comm' (q := true)).1.trans <|
      (intuitionistically_mono h.1).trans <| (intuitionisticallyIf_comm' (q := true)).2.trans <|
      intuitionisticallyIf_mono intuitionistically_and.1

def appM? (e : Expr) (fName : Name) : Option <| Array Expr :=
  if e.isAppOf fName then
    e.getAppArgs
  else
    none

Pure in Init.Prelude

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

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

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

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

instance pureAbsorbing (φ : Prop) [BI PROP] : Absorbing (PROP := PROP) iprop(⌜φ⌝) where
  absorbing := absorbingly_pure.1

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

partial def PMTerm.parse (term : Syntax) : MacroM PMTerm := do
  match ← expandMacros term with
  | `(pmTerm| $trm:term) => return ⟨trm, [], []⟩
  | `(pmTerm| $trm:term with $spats,*) => return ⟨trm, [], ← parseSpats spats⟩
  | `(pmTerm| $trm:term $! $ts,*) => return ⟨trm, ts.getElems.toList, []⟩
  | `(pmTerm| $trm:term $! $ts,* with $spats,*) =>
    return ⟨trm, ts.getElems.toList, ← parseSpats spats⟩
  | _ => Macro.throwUnsupported
where
  parseSpats (spats : Syntax.TSepArray `specPat ",") : MacroM (List SpecPat) :=
      return (← spats.getElems.toList.mapM fun pat => SpecPat.parse pat.raw)

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

def Hyps.mkEmp {prop : Q(Type u)} (bi : Q(BI $prop)) (e := q(BI.emp : $prop)) : Hyps bi e := .emp ⟨⟩

@[simp] def op (s1 s2 : T) : T := merge (K := K) CMRA.op s1 s2

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 [OFE.Discrete α] : CMRA.Discrete (Agree α) where
  discrete_0 := by admit /- proof elided -/

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

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

def ofDiscrete (Equiv : α → α → Prop) (equiv_eqv : Equivalence Equiv) : OFE α where
  Equiv := Equiv
  Dist _ := Equiv
  dist_eqv := equiv_eqv
  equiv_dist := (forall_const _).symm
  dist_lt h _ := h

instance (priority := default - 10) intoAnd_and (p : Bool) [BI PROP] (P Q : PROP) :
    IntoAnd p iprop(P ∧ Q) P Q := ⟨.rfl⟩

def Plainly.plainlyIf [Iris.BI.BIBase PROP] [Plainly PROP] (p : Bool) (P : PROP) : PROP :=
  iprop(if p then ■ P else P)

instance idFree_op_r {x y : α} [IdFree y] [Cancelable x] : IdFree (x • y) where
  id_free0_r z v h :=
    id_free0_r z (validN_op_right v) (cancelableN v (assoc.dist.trans h).symm).symm

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) := ⟨⟩

Fin in Init.Prelude

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

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

instance : Union (State Val) where
  union a b := fun i =>
    match a i, b i with
    | unknown , unknown  => unknown
    | result x, unknown  => result x
    | unknown , result y => result y
    | _       , _        => conflict

instance intoAnd_and_affine_l [BI PROP] (P Q Q' : PROP) [Affine P]
    [h : FromAffinely Q' Q] : IntoAnd false iprop(P ∧ Q) P Q' where
  into_and := (and_mono_l (affine_affinely _).2).trans <|
    affinely_and_l.1.trans <| affinely_and.1.trans <| and_mono (affine_affinely _).1 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

def iff     [BIBase PROP] (P Q : PROP) : PROP := iprop((P → Q) ∧ (Q → P))

let out₂ ← mkFreshExprMVarQ prop
      let _ ← synthInstanceQ q(IntoWand $b $b1 $out $out₁' $out₂)
      let pf := q(specialize_wand $pf $pf')
      return { e := e', hyps := hyps', b := b2, out := out₂, pf }
    else
      
      let v ← mkFreshLevelMVar
      let α : Q(Sort v) ← mkFreshExprMVarQ q(Sort v)
      let Φ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
      let _ ← synthInstanceQ q(IntoForall $out $Φ)
      let x ← elabTermEnsuringTypeQ (u := .succ .zero) arg α
      have out' : Q($prop) := Expr.headBeta q($Φ $x)
      have : $out' =Q $Φ $x := ⟨⟩
      return { e, hyps, b, out := out', pf := q(specialize_forall $pf $x) }

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

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

macro "*" pat:icasesPat : icasesPat => `(icasesPat| ∗ $pat)

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

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

instance [OFE α] [OFE β] [Discrete α] [Discrete β] : Discrete (α × β) where
  discrete_0 H := by admit /- proof elided -/

instance (FF : GFunctors) : GetElem GFunctors (GId FF) COFE.OFunctorPre (fun _ _ => True) where
  getElem _ x _ := (show Array _ from FF)[x.1]

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

class URFunctor (F : COFE.OFunctorPre) where
  
  
  
  [cmra [OFE α] [OFE β] : UCMRA (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 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 -/

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)

Option.map in Init.Prelude

instance Frac_CMRA [Fraction α] : CMRA (Frac α) where
  pcore _ := none
  op := Add.add
  ValidN _ x := Proper x.1
  Valid x := Proper x.1
  op_ne {x} := ⟨fun _ _ _ => congrArg <| Add.add x⟩
  pcore_ne _ := (exists_eq_right'.mpr ·)
  validN_ne H Hp := H ▸ Hp
  valid_iff_validN := forall_const _ |>.symm
  validN_succ := (·)
  validN_op_left := proper_add_mono_left
  assoc := Equiv.of_eq <| by simp only [Add.add]; rw [add_assoc]
  comm := Equiv.of_eq <| by simp only [Add.add]; rw [add_comm]
  pcore_op_left := by admit /- proof elided -/

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

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

inductive SpecPat
  | ident (name : TSyntax ``binderIdent)
  | idents (names : List (TSyntax ``binderIdent)) (goalName : Name)
  deriving Repr, Inhabited
</all_available_defs>

<all_available_lemmas>
theorem exact [BI PROP] (Q : PROP) : Q ⊢ Q

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

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

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

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

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

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

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

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

theorem equiv_none [OFE α] {o : Option α} : o ≡ none ↔ o = none

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

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

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

theorem LimitPreserving.forall [COFE α] (P : β → α → Prop) (Hlim : ∀ y, LimitPreserving (P y)) :
    LimitPreserving (∀ y, P y ·)

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

theorem exclusive_iff {x₁ x₂ : α} (e : x₁ ≡ x₂) : Exclusive x₁ ↔ Exclusive x₂

theorem LimitPreserving.discrete [COFE α] {P : α → Prop} :
    (∀ {x y : α}, x ≡{0}≡ y → (P x → P y)) → LimitPreserving P

theorem proof_example_1 [BI PROP] (P Q R : PROP) (Φ : α → PROP) :
  P ∗ Q ∗ □ R ⊢ □ (R -∗ ∃ x, Φ x) -∗ ∃ x, Φ x ∗ P ∗ Q

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

theorem disjunction [BI PROP] (Q : PROP) : Q ⊢ <affine> (P1 ∨ P2 ∨ P3) -∗ Q

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

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

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

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

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

theorem to_persistent_intuitionistic [BI PROP] {P P' Q : PROP}
    [hP : IntoPersistently true P P'] : Replaces Q iprop(□ P) iprop(□ P')

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

theorem DistLater.dist_lt [OFE α] {m n} {x y : α} (h : DistLater n x y) (hm : m < n) : x ≡{m}≡ y

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

theorem affinelyIf_intro' {p : Bool} [BI PROP] {P Q : PROP} :
    (P ⊢ <affine>?p Q) → <affine>?p P ⊢ <affine>?p Q

theorem and_elim_r_spatial [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd false A A1 A2]
    (h : P ∗ A2 ⊢ Q) : P ∗ A ⊢ Q

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

theorem Update.discrete [CMRA.Discrete α] {x y : α} :
    x ~~> y ↔ ∀ (mz : Option α), ✓ (x •? mz) → ✓ (y •? mz)

theorem map_comp [OFE α] [OFE β] [OFE γ] {f : α -n> β} {g : β -n> γ} {c : Chain α} :
    map (g.comp f) c = map g (map f c)

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

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

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

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

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

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

theorem affinely_true [BI PROP] : <affine> True ⊣⊢ (emp : PROP)

theorem liftRel_eq : liftRel (@Eq α) A B ↔ A = B

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 persistentlyIf_persistently {p : Bool} [BI PROP] {P : PROP} :
    <pers>?p <pers> P ⊣⊢ <pers> P

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

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

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

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

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

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

theorem affine_mono [BI PROP] {P Q : PROP} (h : P ⊢ Q) [Affine Q] : Affine P

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

theorem Whole.not_fractional {a : α} (H : Whole a) : ¬Fractional a

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

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

theorem exact_lean' [BI PROP] (Q : PROP) : Q ⊢ (emp ∗ Q) ∗ emp

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

theorem intuitionisticallyIf_ne {p : Bool} [BI PROP] :
    OFE.NonExpansive (intuitionisticallyIf (PROP := PROP) p)

theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q)]
    (h_rem : P ⊣⊢ P' ∗ A) (h : P' ⊢ Q) : P ⊢ Q

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

@[simp] theorem map_apply [OFE α] [OFE β] {f : α -n> β} {c : Chain α} {n} :
    map f c n = f (c n)

theorem Agree.validN_ne {x y : Agree α} : x ≡{n}≡ y → x.validN n → y.validN n

theorem dist_prod_ext {n} [OFE α] [OFE β] {x₁ x₂ : α} {y₁ y₂ : β}
    (ex : x₁ ≡{n}≡ x₂) (ey : y₁ ≡{n}≡ y₂) : (x₁, y₁) ≡{n}≡ (x₂, y₂)

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

theorem sep_exists_r [BI PROP] {Φ : α → PROP} {Q : PROP} : (∃ a, Φ a) ∗ Q ⊣⊢ ∃ a, Φ a ∗ Q

theorem spatial_elim_spatial [BI PROP] {A A' Q : PROP} [FromAffinely A' A false]
    (h : P ∗ A' ⊢ Q) : P ∗ A ⊢ Q

theorem imp_congr_r [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P → Q) ⊣⊢ (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 affinelyIf_sep_2 {p : Bool} [BI PROP] {P Q : PROP} :
    <affine>?p P ∗ <affine>?p Q ⊢ <affine>?p (P ∗ Q)

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

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

theorem loeb [BI PROP] [BILoeb PROP] {P : PROP} : (▷ P → P) ⊢ P

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

theorem IncludedN.le {n n'} {x y : α} : n' ≤ n → x ≼{n} y → x ≼{n'} y

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

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

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

theorem and_elim_l_spatial [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd false A A1 A2]
    (h : P ∗ A1 ⊢ Q) : P ∗ A ⊢ Q

theorem total_point_inc_point_iff [IsTotal V] : (point i (T := T) (some x)) ≼ (point i (some y)) ↔ x ≼ y

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

theorem bupd_or {P Q: PROP} : iprop((|==> P) ∨ (|==> Q) ⊢ |==> (P ∨ Q))

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

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

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

theorem plainly_impl : ■ (P → Q) ⊢ ■ P → ■ Q

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

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

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

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

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

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

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

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

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

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

theorem Update.prod (x : α × β) (uxy₁ : x.fst ~~> y.fst) (uxy₂ : x.snd ~~> y.snd) : x ~~> y

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

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

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

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

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

theorem uPred_entails_lim {cP cQ : Chain (UPred M)} (H : ∀ n, cP n ⊢ cQ n) :
    IsCOFE.compl cP ⊢ IsCOFE.compl cQ

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

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

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

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

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

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

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

theorem persistently_and_sep_assoc [BI PROP] {P Q R : PROP} :
    <pers> P ∧ (Q ∗ R) ⊣⊢ (<pers> P ∧ Q) ∗ R

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

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

theorem LocalUpdate.prod' {x1 y1 x1' y1' : α} {x2 y2 x2' y2' : β}
    (hl : (x1, y1) ~l~> (x1', y1')) (hr : (x2, y2) ~l~> (x2', y2')) :
    ((x1, x2), (y1, y2)) ~l~> ((x1', x2'), (y1', y2'))

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

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

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

theorem imp_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
    [FromImp Q A1 A2] [inst : IntoPersistently false A1 B] (h : P ∗ □ B ⊢ A2) : P ⊢ Q

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

@[simp] theorem Hom.id_comp [OFE α] [OFE β] {f : α -n> β} : Hom.id.comp f = f

@[simp] theorem BIBase.BiEntails.rfl [BI PROP] {P : PROP} : P ⊣⊢ P

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

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

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

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

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

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

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

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

theorem apply_lean [BI PROP] {P Q R : PROP} (h1 : ⊢ Q) (h2 : P ∗ Q ⊢ R) : P ⊢ R

theorem as_emp_valid_1 [BI PROP] (P : PROP) [AsEmpValid1 φ P] : φ → ⊢ P

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

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

theorem core_inc_self {x : α} [CoreId x] : core x ≼ x

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

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

theorem and [BI PROP] (Q : PROP) : Q ⊢ Q ∧ Q

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

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

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

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

theorem persistently_iff [BI PROP] {P : PROP} [Persistent P] [Absorbing P] :
    <pers> P ⊣⊢ P

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

theorem equivalence_eq : Equivalence (@Eq α)

theorem plainly_into_absorbingly : ■ P ⊢ <absorb> P

theorem affinely_false [BI PROP] : <affine> False ⊣⊢ (False : PROP)

theorem LocalUpdate.alloc_option {x : α} (y : Option α)
    (vx : ✓ x) : (none, y) ~l~> (some x, some x)

theorem intuitionistically_forall_1 [BI PROP] {Φ : α → PROP} : □ (∀ x, Φ x) ⊢ ∀ x, □ Φ x

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

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

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

theorem disjoint_assoc {a b c : State Val} : a ∪ b |

theorem intuitionistically_iff_persistently [BI PROP] [BIAffine PROP]
    {P : PROP} : □ P ⊣⊢ <pers> P

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

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

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

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

theorem persistent_congr [BI PROP] {P Q : PROP} (H : P ⊣⊢ Q) : Persistent P ↔ Persistent Q

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

theorem pcore_validN {n} {x : α} {cx} (e : pcore x = some cx) (v : ✓{n} x) : ✓{n} cx

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

theorem sep [BI PROP] [BIAffine PROP] (Q : PROP) : P1 ∗ P2 ∗ Q ⊢ Q

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

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

theorem imp_elim_r [BI PROP] {P Q : PROP} : P ∧ (P → Q) ⊢ 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 inc_iff_incN [OFE.Discrete α] (n) {x y : α} : x ≼ y ↔ x ≼{n} y

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

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

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

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

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

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

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

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

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

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

theorem ownM_unit P : P ⊢ □ ownM (CMRA.unit : M)

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

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

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

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

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

theorem union_comm {a b : State Val} : a ∪ b = b ∪ a

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

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

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

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

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

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

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

theorem persistently_elim [BI PROP] {P : PROP} [Absorbing P] : <pers> P ⊢ P

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

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

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

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

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

@[simp] theorem not_some_dist_none [OFE α] {n} {x : α} : ¬some x ≡{n}≡ none

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

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

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

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

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

theorem mp [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q → R) (h2 : P ⊢ Q) : P ⊢ R
</all_available_lemmas>

<local_ctx>
import Iris.Algebra.OFE

namespace Iris.COFE.OFunctor

open OFE

variable {F : ∀ α β [OFE α] [OFE β], Type u} [OFunctorContractive F]

variable [∀ α [COFE α], IsCOFE (F α α)]

variable [inh : Inhabited (F (ULift Unit) (ULift Unit))]

namespace Fix.Impl

variable (F) in

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

variable (F) in

def A (n : Nat) : Type u := (A' F n).1

variable (F) in

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

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

end

  open OFunctorContractive in exact match k with
  | 0 => map_contractive.zero (x := (_, _)) (y := (_, _)) _ _
  | k+1 => map_contractive.succ (x := (_, _)) (y := (_, _)) _ ⟨up_down, up_down⟩ _

variable (F) in

@[ext] structure Tower : Type u where
  val k : A F k
  protected down {k} : down F k (val (k+1)) ≡ val k

variable (F) in

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

variable (F) in

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

def eqToHom (e : i = k) : A F i -n> A F k := e ▸ .id

def embed : A F k -n> A F i :=
  if h : k ≤ i then (eqToHom (Nat.add_sub_cancel' h)).comp (upN ..)
  else (downN ..).comp (eqToHom (Nat.add_sub_cancel' (Nat.le_of_not_ge h)).symm)

protected def Tower.embed (k) : A F k -n> Tower F :=
</local_ctx>

<target_theorem>
theorem Tower.embed_up (x : A F k) :
    Tower.embed (k+1) (up F k x) ≡ Tower.embed k x :=
</target_theorem>

