## Stream: new members

### Topic: Simplifying out logical junk

#### Ken Roe (Jul 28 2018 at 01:22):

How can the following theorem be proven:

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


#### Simon Hudon (Jul 28 2018 at 01:29):

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

Last updated: May 06 2021 at 22:13 UTC