+taggare le meta con tag::Type e in sort_of_prod verificare che i Pi
+tra meta coinvolgano meta taggate. Il tag potrebbe contenere un bound,
+in modo che si possano taggare anche meta quando si unifica ? ==vs== Type_k
+e la si tagga con bound a seconda del test_eq_only <= k.