2 Théorème de non incohérence de lazi.1.0
Contexte
Les preuves en lazi.1.0 sont traduisiblesen preuves lazi.0.0 (reste à prouver), donc la cohérence de lazi.0.0 se communique à lazi.1.0.
Énoncé
Il est absurde que lazi.1.0 soit incohérente.
Preuve
Supposons que 1b = 0b soit démontrable en lazi.1.0.
Soit p une preuve lazi.0.1 de 1b = 0b. Comme toute preuve lazi.0.1 est traduisible en preuve lazi.0.0 (reste à prouver), il existe une preuve q lazi.0.0 de 1b = 0b. On obtient alors une absurdité par la cohérence de lazi.0.0.
@todo
@theorem