TODO
NUCLEO
+ - CRITICO (trovato anche da Ferruccio): typechecking di
+ cic:/Coq/ring/Ring_normalize/index_eq_prop.con
+ asserzione del nucleo (applicazione senza argomenti)
- PREOCCUPANTE: per
inductive i : Prop := K : True (*-> i*) -> i.
noi generiamo i_rec e i_rect con e senza il commento qui sopra; Coq NON