exact map_append f g h (xs₁:=xs₁) (xs₂:=xs₂)
α : Type u₁
β : Type u₂
γ : α → β → Type v
α₁ : Type u_1
β₁ : Type u_2
γ₁ : α₁ → β₁ → Type u_3
f : α → α₁
g : β → β₁
h : {a : α} → {b : β} → γ a b → γ₁ (f a) (g b)
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : β
tail✝ x✝ : List β
a✝ : γ head✝¹ head✝
xs₁ : DVect2 γ tail✝¹ tail✝
xs₂ : DVect2 γ x✝¹ x✝
⊢ map f g (fun {a} {b} ↦ h) (append xs₁ xs₂) ≡ append (map f g (fun {a} {b} ↦ h) xs₁) (map f g (fun {a} {b} ↦ h) xs₂)
no goals