Description: Deduction associated with notnotr and notnotri . Double negation
elimination rule. A translation of the natural deduction rule -. -.
C , _G |- -. -. ps => _G |- ps ; see natded . This is Definition
NNC in Pfenning p. 17. This rule is valid in classical logic (our
logic), but not in intuitionistic logic. (Contributed by DAW, 8-Feb-2017)