NUCLEO
- CRITICO (trovato anche da Ferruccio): typechecking di
cic:/Coq/ring/Ring_normalize/index_eq_prop.con
- asserzione del nucleo (applicazione senza argomenti)
+ asserzione del nucleo (applicazione senza argomenti).
+ Fissare e poi fare una passata su tutto il db.
- 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