apply DVect2.Eq.descend rfl
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ cons (g a) (dfromList f₁ f₂ g (as ++ bs)) ≡ cons (g a) (dfromList f₁ f₂ g as ++ dfromList f₁ f₂ g bs)
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ dfromList f₁ f₂ g (as ++ bs) ≡ dfromList f₁ f₂ g as ++ dfromList f₁ f₂ g bs