Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ nth (cons (head l) (tail l)) (n + 1) = nth (tail l) n
Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ nth l (n + 1) = nth (tail l) n
conv => lhs; rw [← ListBlank.cons_head_tail l]
no goals
Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ nth (cons (head l) (tail l)) (n + 1) = nth (tail l) n
exact Quotient.inductionOn' l.tail fun l ↦ rfl