best way to prove

Stream: new members

[Arjun Pitchanathan]

What's the best way to prove this? I have a proof (strong induction on l1.length) but it's upwards of a hundred lines...

import data.list
noncomputable theory
open_locale classical
universe u
variables (α β : Type u)
example {l₁ l₂ : list β} {r : α → β → Prop} (nodup : ∀ (x y : α) (b : β),
    x ≠ y → ¬ (r x b ∧ r y b)) : (∀ a : α, l₁.countp (r a) = l₂.countp (r a)) →
    l₁.countp (λ b, ∃ a, r a b) = l₂.countp (λ b, ∃ a, r a b) := sorry

[Bryan Gin-ge Chen]

I took a crack at this but I wasn't able to succeed. Can you post your proof or link to a gist?

[Arjun Pitchanathan]

Here it is. I'm not sure how readable it is. I tried to add some explanatory comments.