in are_convertible togliere il caso Prop,Prop in quanto catturato da ===
in are_convertible togliere il caso Meta,Meta in quanto catturato da ===
in are_convertible caso Meta,Meta non fare lift ma accorcia il ctx
+
+
+
+-------
+?1 = t
+ (?1,?2)::(?2,t)::subst
+ where ctx ?2 è minimale per t
+ poi le subst (?n,?m) le risolvi subito