no goals
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
n : ℕ
⊢ ListBlank.nth (right₀ T) n = nth T ↑n
cases n <;> simp only [Tape.nth, Tape.right₀, Int.ofNat_zero, ListBlank.nth_zero,
  ListBlank.nth_succ, ListBlank.head_cons, ListBlank.tail_cons, Nat.zero_eq]