(*#* This file formalizes Berardi's paradox which says that in
the calculus of constructions, excluded middle (EM) and axiom of
(*#* This file formalizes Berardi's paradox which says that in
the calculus of constructions, excluded middle (EM) and axiom of