Simplifying out logical junk

Stream: new members

[Ken Roe]

How can the following theorem be proven:

theorem junk { p : Prop } { q : Prop } : (p ∨ (q → false))=p :=
begin
    sorry
end

[Simon Hudon]

I don't think the theorem hold. If p is false and q is false too, the left hand side is true and the right hand side is false