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>
inductive Ty
  | bool
  | nat

inductive Value : Ty → Type
  | bool : Bool → Value .bool
  | nat  : Nat  → Value .nat

instance : Coe Bool (Value .bool) where
  coe := .bool

inductive Term : Ty → Type
  | val (v : Value τ)                          : Term τ
  | ite (cond : Term .bool) (pos neg : Term τ) : Term τ
  | and (lhs rhs : Term .bool)                 : Term .bool

instance : Coe (Value τ) (Term τ) where
  coe := val

def eval : Term τ → Value τ
  | val v => v
  | ite cond pos neg =>
    match eval cond with
    | true  => eval pos
    | false => eval neg
  | and lhs rhs =>
    match eval lhs, eval rhs with
    | true, true => true
    | _,    _    => false

def constFold : Term τ → Term τ
  | val v                             => val v
  | ite cond pos neg                  => ite (constFold cond) (constFold pos) (constFold neg)
  | and true true                     => true
  | and (Value.bool _) (Value.bool _) => false
  | and lhs rhs                       => and (constFold lhs) (constFold rhs)

def Equiv (t₁ t₂ : Term τ) : Prop :=
  eval t₁ = eval t₂

inductive Instruction
  | const (n : Nat)
  | and
  | jmp (offset : Nat)
  | jez (offset : Nat)

abbrev Program := List Instruction

abbrev Stack := List Nat

def Nat.conj : Nat → Nat → Nat
  | 0, _ | _, 0 => 0
  | _, _        => 1

structure Instruction.Result where
  stack : Stack
  offset := 0

def Instruction.exec : Instruction → Stack → Option Instruction.Result
  | .const n,    stack        => some { stack := n :: stack }
  | .and,        r :: l :: tl => some { stack := (l.conj r) :: tl }
  | .and,        _            => none
  | .jmp offset, stack        => some { stack, offset }
  | .jez offset, 0 :: tl      => some { stack := tl, offset }
  | .jez _,      _ :: tl      => some { stack := tl }
  | .jez _,      _            => none

def goto : Program → Nat → Option Program
  | prog,    0          => prog
  | [],      _ + 1      => none
  | _ :: tl, offset + 1 => goto tl offset

def exec : Program → Stack → Option Stack
  | [],       stack => stack
  | hd :: tl, stack =>
    match Instruction.exec hd stack with
    | none => none
    | some { stack, offset } =>
      match h : goto tl offset with
      | none   => none
      | some p => exec p stack
termination_by p => p.length
decreasing_by simp +arith [goto_decreasing h]

def Value.toNat : Value τ → Nat
  | bool false => 0
  | bool true  => 1
  | nat n      => n

def Term.lower : Term τ → Program
  | val v            => [.const v.toNat]
  | and lhs rhs      => (lower lhs) ++ (lower rhs) ++ [.and]
  | ite cond pos neg =>
    let p := lower pos
    let n := lower neg
    lower cond ++ [.jez (p.length + 1)] ++ p ++ [.jmp n.length] ++ n

def HEquiv (t : Term τ) (prog : Program) : Prop :=
  prog.exec [] = some [t.eval.toNat]

def compile (t : Term τ) : Program :=
  lower (constFold t)

Bool in Init.Prelude

Nat in Init.Prelude

bool in Init.Control.Basic

Coe in Init.Coe

cond in Init.Prelude

List in Init.Prelude

Option in Init.Prelude

List.cons in Init.Prelude

List.next in Mathlib.Data.List.Cycle
</all_available_defs>

<all_available_lemmas>
@[simp]
theorem eval_val_eq_val (v : Value τ) : eval v = v

theorem ite_congr (hc : c₁ ~ c₂) (hp : p₁ ~ p₂) (hn : n₁ ~ n₂) : ite c₁ p₁ n₁ ~ ite c₂ p₂ n₂

theorem and_congr (hl : l₁ ~ l₂) (hr : r₁ ~ r₂) : and l₁ r₁ ~ and l₂ r₂

@[simp]
theorem and_true : and true true ~ true

@[simp]
theorem and_false (h : b₁ = false ∨ b₂ = false) : and b₁ b₂ ~ false

theorem constFold_equiv (t : Term τ) : t ~ constFold t

theorem goto_decreasing {p : Program} (h : p.goto offset = some p') : p'.length ≤ p.length

theorem HEquiv.equiv_congr (ht : t₁ ~ t₂) (hp : t₁ ≈ prog) : t₂ ≈ prog

@[simp]
theorem exec_stack_mono (s : Stack) (h : exec inst s₁ = some ⟨s₂, o⟩) :
    exec inst (s₁ ++ s) = some ⟨s₂ ++ s, o⟩

@[simp]
theorem exec_stack_mono (s : Stack) (h : exec prog s₁ = some s₂) :
    exec prog (s₁ ++ s) = s₂ ++ s

@[simp]
theorem toNat_conj_eq_eval_and_toNat (lhs rhs : Term .bool) :
    (and lhs rhs).eval.toNat = Nat.conj lhs.eval.toNat rhs.eval.toNat

theorem lower_val_hEquiv (v : Value τ) : val v ≈ lower (val v)

theorem lower_and_hEquiv (hl : lhs ≈ lower lhs) (hr : rhs ≈ lower rhs) :
    and lhs rhs ≈ lower (and lhs rhs)
</all_available_lemmas>

<local_ctx>
inductive Ty
  | bool
  | nat

inductive Value : Ty → Type
  | bool : Bool → Value .bool
  | nat  : Nat  → Value .nat

inductive Term : Ty → Type
  | val (v : Value τ)                          : Term τ
  | ite (cond : Term .bool) (pos neg : Term τ) : Term τ
  | and (lhs rhs : Term .bool)                 : Term .bool

namespace Term

def eval : Term τ → Value τ
  | val v => v
  | ite cond pos neg =>
    match eval cond with
    | true  => eval pos
    | false => eval neg
  | and lhs rhs =>
    match eval lhs, eval rhs with
    | true, true => true
    | _,    _    => false

namespace Equiv

infixl:50 " ~ " => Equiv

end Equiv

end Term

open Term (eval)

inductive Instruction
  | const (n : Nat)
  | and
  | jmp (offset : Nat)
  | jez (offset : Nat)

abbrev Program := List Instruction

abbrev Stack := List Nat

def Nat.conj : Nat → Nat → Nat
  | 0, _ | _, 0 => 0
  | _, _        => 1

structure Instruction.Result where
  stack : Stack
  offset := 0

def Instruction.exec : Instruction → Stack → Option Instruction.Result
  | .const n,    stack        => some { stack := n :: stack }
  | .and,        r :: l :: tl => some { stack := (l.conj r) :: tl }
  | .and,        _            => none
  | .jmp offset, stack        => some { stack, offset }
  | .jez offset, 0 :: tl      => some { stack := tl, offset }
  | .jez _,      _ :: tl      => some { stack := tl }
  | .jez _,      _            => none

namespace Program

def goto : Program → Nat → Option Program
  | prog,    0          => prog
  | [],      _ + 1      => none
  | _ :: tl, offset + 1 => goto tl offset

def exec : Program → Stack → Option Stack
  | [],       stack => stack
  | hd :: tl, stack =>
    match Instruction.exec hd stack with
    | none => none
    | some { stack, offset } =>
      match h : goto tl offset with
      | none   => none
      | some p => exec p stack
termination_by p => p.length
decreasing_by simp +arith [goto_decreasing h]

end Program

def Value.toNat : Value τ → Nat
  | bool false => 0
  | bool true  => 1
  | nat n      => n

def Term.lower : Term τ → Program
  | val v            => [.const v.toNat]
  | and lhs rhs      => (lower lhs) ++ (lower rhs) ++ [.and]
  | ite cond pos neg =>
    let p := lower pos
    let n := lower neg
    lower cond ++ [.jez (p.length + 1)] ++ p ++ [.jmp n.length] ++ n

def HEquiv (t : Term τ) (prog : Program) : Prop :=
  prog.exec [] = some [t.eval.toNat]

infixl:60 " ≈ " => HEquiv

namespace Instruction

end Instruction

namespace Program

end Program

namespace Term

open Program List

open Instruction hiding exec
</local_ctx>

<target_theorem>
theorem lower_ite_hEquiv {cond : Term .bool} {pos neg : Term τ}
    (hc : cond ≈ lower cond) (hp : pos ≈ lower pos) (hn : neg ≈ lower neg) :
    ite cond pos neg ≈ lower (ite cond pos neg) :=
</target_theorem>

