X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fcpy.ma;h=d6959e253f22ac5013d56acdb36e6fe8471ecc2a;hb=46a8a345410219548128c2533ce32b1a8eca6c06;hp=e1b2afd754ef86043369bd39e3b45aa7e0ea7922;hpb=6907a0f66a3782ce4273a609203c9b574841c7d1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
index e1b2afd75..d6959e253 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
@@ -20,17 +20,18 @@ include "basic_2/relocation/lsuby.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL SUBSTITUTION FOR TERMS ***************)
 
+(* Note: this substitution is ordinary *)
 (* activate genv *)
 inductive cpy: nat → nat → relation4 genv lenv term term ≝
 | cpy_atom : ∀I,G,L,d,e. cpy d e G L (⓪{I}) (⓪{I})
 | cpy_subst: ∀I,G,L,K,V,W,i,d,e. d ≤ i → i < d + e →
              ⇩[0, i] L ≡ K.ⓑ{I}V → ⇧[0, i + 1] V ≡ W → cpy d e G L (#i) W
 | cpy_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
-             cpy d e G L V1 V2 → cpy (d + 1) e G (L.ⓑ{I} V2) T1 T2 →
-             cpy d e G L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
+             cpy d e G L V1 V2 → cpy (d + 1) e G (L.ⓑ{I}V2) T1 T2 →
+             cpy d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
 | cpy_flat : ∀I,G,L,V1,V2,T1,T2,d,e.
              cpy d e G L V1 V2 → cpy d e G L T1 T2 →
-             cpy d e G L (ⓕ{I}V1. T1) (ⓕ{I}V2. T2)
+             cpy d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
 .
 
 interpretation "context-sensitive extended parallel substritution (term)"