rcases with false

Stream: new members

[Kenny Lau]

Can I do rcases on p \or false and end up with one state where we know p?

[Reid Barton]

Well rcases t with t'|⟨⟨⟩⟩ seems to work but I don't know if I would really advise it

[Kenny Lau]

would @Mario Carneiro advise it?

[Simon Hudon]

That looks like something I would do

[Chris Hughes]

I'm sure or_false is a lemma. Use that.

[Kenny Lau]

yes. but this is just a minimal example.

[Mario Carneiro]

I would advise it; if you search for that (with spaces around the | ) you will find me use it in several places