X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flsubc.ma;h=0af4368e39a6b59f271b7e80fffd1f5329f45219;hb=ebc33b6d5b68400bc8411973ed4c9ed50d0c52a6;hp=ee9d5df166d1b4403bb4f745d7d2389a862bce00;hpb=65008df95049eb835941ffea1aa682c9253c4c2b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma
index ee9d5df16..0af4368e3 100644
--- 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/crsubeq_3.ma".
+include "basic_2/notation/relations/lrsubeq_3.ma".
 include "basic_2/static/aaa.ma".
 include "basic_2/computation/acp_cr.ma".
 
@@ -20,14 +20,14 @@ include "basic_2/computation/acp_cr.ma".
 
 inductive lsubc (RP:lenv→predicate term): relation lenv ≝
 | lsubc_atom: lsubc RP (⋆) (⋆)
-| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. ⓑ{I} V) (L2. ⓑ{I} V)
+| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1.ⓑ{I}V) (L2.ⓑ{I}V)
 | lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ ϵ[RP] 〚A〛 → ⦃L1, W⦄ ϵ[RP] 〚A〛 → L2 ⊢ W ⁝ A →
-              lsubc RP L1 L2 → lsubc RP (L1. ⓓⓝW.V) (L2. ⓛW)
+              lsubc RP L1 L2 → lsubc RP (L1. ⓓⓝW.V) (L2.ⓛW)
 .
 
 interpretation
   "local environment refinement (abstract candidates of reducibility)"
-  'CrSubEq L1 RP L2 = (lsubc RP L1 L2).
+  'LRSubEq RP L1 L2 = (lsubc RP L1 L2).
 
 (* Basic inversion lemmas ***************************************************)
 
@@ -44,7 +44,7 @@ lemma lsubc_inv_atom1: ∀RP,L2. ⋆ ⊑[RP] L2 → L2 = ⋆.
 /2 width=4 by lsubc_inv_atom1_aux/ qed-.
 
 fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
-                          (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I}X) ∨
+                          (∃∃K2. K1 ⊑[RP] K2 & L2 = K2.ⓑ{I}X) ∨
                           ∃∃K2,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
                                       K1 ⊑[RP] K2 &
                                       L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
@@ -60,7 +60,7 @@ lemma lsubc_inv_pair1: ∀RP,I,K1,L2,X. K1.ⓑ{I}X ⊑[RP] L2 →
                        (∃∃K2. K1 ⊑[RP] K2 & L2 = K2.ⓑ{I}X) ∨
                        ∃∃K2,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
                                    K1 ⊑[RP] K2 &
-                                   L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
+                                   L2 = K2.ⓛW & X = ⓝW.V & I = Abbr.
 /2 width=3 by lsubc_inv_pair1_aux/ qed-.
 
 fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → L2 = ⋆ → L1 = ⋆.
@@ -75,11 +75,11 @@ qed-.
 lemma lsubc_inv_atom2: ∀RP,L1. L1 ⊑[RP] ⋆ → L1 = ⋆.
 /2 width=4 by lsubc_inv_atom2_aux/ qed-.
 
-fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
+fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2.ⓑ{I} W →
                           (∃∃K1. K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨
                           ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
                                     K1 ⊑[RP] K2 &
-                                    L1 = K1. ⓓⓝW.V & I = Abst.
+                                    L1 = K1.ⓓⓝW.V & I = Abst.
 #RP #L1 #L2 * -L1 -L2
 [ #I #K2 #W #H destruct
 | #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
@@ -88,7 +88,7 @@ fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2. ⓑ
 qed-.
 
 (* Basic_1: was just: csubc_gen_head_l *)
-lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 ⊑[RP] K2. ⓑ{I} W →
+lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 ⊑[RP] K2.ⓑ{I} W →
                        (∃∃K1. K1 ⊑[RP] K2 & L1 = K1.ⓑ{I} W) ∨
                        ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
                                  K1 ⊑[RP] K2 &