apply DVect2.Eq.trans (DVect2.join_append fs _) _
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join (fs ++ join fsss) ≡ join fs ++ join (map List.join List.join (fun {a} {b} ↦ join) fsss)
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join fs ++ join (join fsss) ≡ join fs ++ join (map List.join List.join (fun {a} {b} ↦ join) fsss)