dsimp [DVect2.join, DVect2.map]
α : 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 (join (cons fs fsss)) ≡ join (map List.join List.join (fun {a} {b} ↦ join) (cons fs 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 fsss) ≡ join fs ++ join (map List.join List.join (fun {a} {b} ↦ join) fsss)