How to close proof on BitBlasting over Fin

Stream: new members

[Bernardo Borges]

Hello everyone
I'm working on discharging problems on BitVectors to SAT, and I'm trying to encode their definitions in terms of Fin. Below you can see how I define a bbT. How can I close this inductive proof? I have tried using match on the bitvec, but you don't have "match_pattern" on the nil-cons structure, since bitvec is defined as a Fin of 2^w:

import Mathlib

open BitVec

def bbT {w : ℕ} (v : Fin w → Bool) : BitVec w := match w with
| 0     => 0#0
| (s+1) => cons (v s) (bbT (λi↦v i))

def bbVar (x : BitVec w) : x = bbT (λi↦x[i]) := by
  induction w with
  | zero => exact eq_of_getMsbD_eq (congrFun rfl)
  | succ s hi =>
      unfold bbT
      simp only [Fin.natCast_eq_last, Fin.getElem_fin, Fin.val_last, Fin.coe_eq_castSucc, Fin.coe_castSucc]
      -- s : ℕ
      -- hi : ∀ (x : BitVec s), x = bbT fun i => x[i]
      -- x : BitVec (s + 1)
      -- ⊢ x = cons x[s] (bbT fun i => x[↑i])
      sorry

You can see the full code here