X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpreterm_dephi.ma;h=60c5a4a41f7bdf191bc194a4a7460607c0ea8efb;hb=ec5739f16f3d23d26dd2528bf20df21919580e0f;hp=67aa029d70af910f5833f87c9dba5dec5658d18f;hpb=c8ba3d001893666a52c393d9cf8a0929dacd007a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma
index 67aa029d7..60c5a4a41 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma
@@ -12,9 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "delayed_updating/syntax/path_dephi.ma".
 include "delayed_updating/syntax/preterm_constructors.ma".
 
 (* DEPHI FOR PRETERM ********************************************************)
 
-definition preterm_dephi (f) (t) ≝
-           λp. ∃∃q. q ϵ⬦ t & p = path_dephi f q. 
+definition preterm_dephi (f) (t): preterm ≝
+           λp. ∃∃q. q ϵ t & p = path_dephi f q.