X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Ffleq.ma;h=da608196ccbd2b8e823bbbed1428038511564eb5;hb=c9a1672c725945b47f9ea8af3c23b67cf9026f01;hp=2448b5260e643c94863d25b93d040cfd3e9b0b8e;hpb=dec157aae89a4c1830f18eeb0b4152c8c5162ca7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma
index 2448b5260..da608196c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/fleq_8.ma".
+include "basic_2/notation/relations/lazyeq_8.ma".
 include "basic_2/computation/lpxs.ma".
 
 (* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************)
@@ -24,7 +24,7 @@ definition fleq: ∀h. sd h → tri_relation genv lenv term ≝
 
 interpretation
    "equivalent 'big tree' normal forms (closure)"
-   'FLEq h g G1 L1 T1 G2 L2 T2 = (fleq h g G1 L1 T1 G2 L2 T2).
+   'LazyEq h g G1 L1 T1 G2 L2 T2 = (fleq h g G1 L1 T1 G2 L2 T2).
 
 (* Basic_properties *********************************************************)