some renaming and some typos corrected ...

[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..f45319f6746524afa959f9dd70a37bd6a25a11ac 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".
 
@@ -21,13 +21,13 @@ include "basic_2/computation/acp_cr.ma".
 inductive lsubc (RP) (G): relation lenv ≝
 | lsubc_atom: lsubc RP G (⋆) (⋆)
 | lsubc_pair: ∀I,L1,L2,V. lsubc RP G L1 L2 → lsubc RP G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubc_abbr: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A →
+| lsubc_beta: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A →
               lsubc RP G L1 L2 → lsubc RP G (L1. ⓓⓝW.V) (L2.ⓛW)
 .
 
 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 ***************************************************)