update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / preterm_dephi.ma

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 67aa029d70af910f5833f87c9dba5dec5658d18f..60c5a4a41f7bdf191bc194a4a7460607c0ea8efb 100644 (file)
--- 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.