exact DVect2.Eq.descend rfl (append_nil 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
no goals