Discharges an assumption, transforming |- s ==> F into |- ~s.
DESCRIPTION
When applied to a term s and a theorem A |- t, the inference
rule NEG_DISCH returns the theorem A - {s} |- s ==> t, or if t
is just F, returns the theorem A - {s} |- ~s.
A |- F
-------------------- NEG_DISCH [special case]
A - {s} |- ~s
A |- t
-------------------- NEG_DISCH [general case]
A - {s} |- s ==> t