update in ground_2, web page for ground_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / fleq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma
index 2448b5260e643c94863d25b93d040cfd3e9b0b8e..da608196ccbd2b8e823bbbed1428038511564eb5 100644 (file)
--- 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 *********************************************************)