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