no goals
Γ : Type u_3
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_1
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
S : Finset Λ'
l : List Bool
q : Stmt Bool Λ' σ
⊢ SupportsStmt S (write l q) = SupportsStmt S q
induction' l with _ l IH <;> simp only [write, SupportsStmt, *]