rw [cons_append]
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ : List α
head✝ : β
tail✝ : List β
f : γ head✝¹ head✝
fs : DVect2 γ tail✝¹ tail✝
⊢ cons f fs ++ nil ≡ cons f fs
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ : List α
head✝ : β
tail✝ : List β
f : γ head✝¹ head✝
fs : DVect2 γ tail✝¹ tail✝
⊢ cons f (fs ++ nil) ≡ cons f fs