In systems with the falsum this rule allows inferring the a claim when the falsum can be derived from the assumption of its negation. In systems without the falsum it expresses the classical Reductio Ad Absurdum coupled, as is the falsum version, with Double Negation Elimination.
Preview shown for the Typed Forward Strict derivation type in the LRC_O system