intro b₁ b₂ hb₁ hb₂
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ ∀ (a_1 b : β), decide (f a = a_1) = true → decide (f a = b) = true → a_1 = b
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
b₁ b₂ : β
hb₁ : decide (f a = b₁) = true
hb₂ : decide (f a = b₂) = true
⊢ b₁ = b₂