1. up to Fatou lemma (almost there)
2. requires the new unification procedure for coercions to enable
multiple coercion paths between two nodes
3. it stresses CicUniv.mere_ugraphs. To compile the new DAMA file quickly
you have to disable that function :-(