How to better use "let"?

Stream: general

[Jiatong Yang]

import tactic
axiom Set : Type
axiom mem : Set → Set → Prop -- flipped ∈
axiom describe (p : Set → Prop) : ∃ s, p = mem s
theorem contra : false := begin
  let p := λ x, ¬ mem x x,
  cases describe p with s h,
  have T : p s = mem s s := by rw h,
  have K : (λ x, ¬ mem x x) s = mem s s := T,
  finish,
end

I think 8th & 9th lines are tediously long. How to improve that?

[Alex J. Best]

You can zip the whole thing down to:

import tactic
axiom Set : Type
axiom mem : Set → Set → Prop -- flipped ∈
axiom describe (p : Set → Prop) : ∃ s, p = mem s
theorem contra : false := begin
  cases describe (λ x, ¬ mem x x) with s h,
  simpa using congr_fun h s,
end