From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 24 Sep 2008 16:37:42 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4744
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=84762225fd1bbacf9d9ce7d1fe259a4dd17f4351;p=helm.git

...
---

diff --git a/helm/software/components/ng_kernel/TODO b/helm/software/components/ng_kernel/TODO
index 4511bbae0..ed64039cb 100644
--- 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