- more background for the exclusion binder

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lifts_vector.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
index 8acd0a571249d2c4332d87ccbaf016c589c53a22..62af6ac90ca762e0090018eb5e3dddb8f2f0678d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
@@ -25,10 +25,10 @@ inductive liftsv (f:rtmap): relation (list term) ≝
                liftsv f (T1 @ T1s) (T2 @ T2s)
 .
 
-interpretation "uniform relocation (vector)"
+interpretation "uniform relocation (term vector)"
    'RLiftStar i T1s T2s = (liftsv (uni i) T1s T2s).
 
-interpretation "generic relocation (vector)"
+interpretation "generic relocation (term vector)"
    'RLiftStar f T1s T2s = (liftsv f T1s T2s).
 
 (* Basic inversion lemmas ***************************************************)