## Stream: new members

### Topic: best way to prove

#### Arjun Pitchanathan (Mar 03 2020 at 02:49):

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 (Mar 03 2020 at 19:56):

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 (Mar 03 2020 at 20:33):

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

Last updated: May 08 2021 at 19:11 UTC