二重否定導入

$ A \models \lnot\lnot A