The notR proof rule proves a negation ¬P by instead assuming its opposite P. In the case of an empty Δ, this directly corresponds to proving a negation ¬P by proving a contradiction (false) from the opposite assumption P.
See also
prop uses all propositional logic rules for operators ¬,∧,∨,→,↔
unfold does all easy steps until loop or ODE without excessive branching