+ - coercions verso sorte:
+ 1. coercere a una sorta in posizione controvariante: andare verso Prop,
+ altrimenti verso {Type,Set,CProp} (indifferentemente?)
+ 2. coercere a una sorta in posizione covariante: la scelta piu' safe e'
+ andare verso Type, poi verso CProp, poi verso Set, poi verso Prop.
+ Unico problema: la scelta piu' safe e' anche quella pessima dal punto
+ di vista dell'estrazione di codice :-(
+ - fare normalize_pattern : pattern -> goal -> pattern e usarla per
+ abilitare fase 2 in fold e rewrite
+ - apply puo' generare termini non ben tipati.
+ Esempio: p = q e fare apply eq_ind' di p!