X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FTODO;h=02913a155a14729973b80b7c9c56606a349f3723;hb=cf60cad5ad896f358d6e8dd2ded1c0430ba2c55c;hp=cfe8ca1171b17457c49593d977fde8e018289717;hpb=761aef3c864626e17004b9785c39def7053271e0;p=helm.git

diff --git a/helm/software/components/ng_kernel/TODO b/helm/software/components/ng_kernel/TODO
index cfe8ca117..02913a155 100644
--- a/helm/software/components/ng_kernel/TODO
+++ b/helm/software/components/ng_kernel/TODO
@@ -13,6 +13,8 @@ e la si tagga con bound a seconda del test_eq_only <= k.
 nel vecchio nucleo la height_of di un b-redex fa 0 e quindi riduci in forma
 normale. Spostare la small_delta_step. 
 
+
+@ tra universi senza duplicati
 -------
 ?1 = t
   (?1,?2)::(?2,t)::subst