...

diff --git a/helm/software/components/ng_kernel/TODO b/helm/software/components/ng_kernel/TODO
index 4511bbae0e5ff53353992fee4630389d434fe20a..ed64039cbb36a1199e3d411e8aa1c481805a3c9e 100644 (file)
--- a/helm/software/components/ng_kernel/TODO
+++ b/helm/software/components/ng_kernel/TODO
@@ -2,3 +2,11 @@ muovere la split_prods nella riduzione e usarla nel caso di convertibilità di 2
 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