halp.lean

open classical

variables (α : Type) (p q : α → Prop)
variable a : α
variable r : Prop

example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) := 
iff.intro
  (λ ⟨a, hpa⟩, (λ ax, ax a hpa))
  (λ nanpx : (∀ x, p x → false) → false,
    suffices hpa : p a, from ⟨a, hpa⟩,
    by_contradiction
      (λ hnpa,
        nanpx (λ ha, hnpa))
    -- type mismatch at application
    --   nanpx (λ (ha : α), hnpa)
    -- term
    --   λ (ha : α), hnpa
    -- has type
    --   α → ¬p a
    -- but is expected to have type
    --   ∀ (x : α), p x → false
  )