2014-07-25 08:30:30 -07:00
|
|
|
import logic
|
|
|
|
|
|
2015-04-21 19:33:21 -07:00
|
|
|
section
|
2014-07-25 08:30:30 -07:00
|
|
|
hypothesis P : Prop.
|
|
|
|
|
|
2014-08-26 09:12:18 -07:00
|
|
|
definition crash
|
2014-07-25 08:30:30 -07:00
|
|
|
:= assume H : P,
|
|
|
|
|
have H' : ¬ P,
|
|
|
|
|
from H,
|
|
|
|
|
_.
|
|
|
|
|
|
2014-10-11 17:13:33 -07:00
|
|
|
end
|
