- name changes in the rediction rules

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma
index e43f81978f3f7e61c233a7faec5ab4c5f51a5b0c..ccc10293373fffe39d5daa68e03ca55d2a7d4be9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/lrsubeq_4.ma".
+include "basic_2/notation/relations/lrsubeqc_4.ma".
 include "basic_2/static/aaa.ma".
 include "basic_2/computation/acp_cr.ma".
 
@@ -27,7 +27,7 @@ inductive lsubc (RP) (G): relation lenv ≝
 
 interpretation
   "local environment refinement (abstract candidates of reducibility)"
-  'LRSubEq RP G L1 L2 = (lsubc RP G L1 L2).
+  'LRSubEqC RP G L1 L2 = (lsubc RP G L1 L2).
 
 (* Basic inversion lemmas ***************************************************)