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
10 (?1,?2)::(?2,t)::subst
11 where ctx ?2 è minimale per t
12 poi le subst (?n,?m) le risolvi subito