no goals
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.363898
inst✝¹ : Inhabited Λ
σ : Type ?u.363904
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
⊢ trTape enc0 (Tape.mk' L R) = trTape' enc0 L R
simp only [trTape, Tape.mk'_left, Tape.mk'_right₀]