generated at
二重否定除去
double-negation elimination

\lnot\lnot P\to P