no goals
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : NodupKeys l₁
nd₂ : NodupKeys l₂
p : l₁ ~ l₂
⊢ lookupAll a l₁ = lookupAll a l₂
simp [lookupAll_eq_dlookup, nd₁, nd₂, perm_dlookup a nd₁ nd₂ p]