helm/software/components/ng_kernel/TODO

   1 muovere la split_prods nella riduzione e usarla nel caso di convertibilità di 2 match
   2 in are_convertible togliere il caso Prop,Prop in quanto catturato da ===
   3 in are_convertible togliere il caso Meta,Meta in quanto catturato da ===
   4 in are_convertible caso Meta,Meta non fare lift ma accorcia il ctx
   5
   6
   7
   8 -------
   9 ?1 = t
  10   (?1,?2)::(?2,t)::subst
  11   where ctx ?2 è minimale per t
  12   poi le subst (?n,?m) le risolvi subito