- notation (possibly affecting all .ma files):

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / unfold / ltpss.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma
index 1baa893e4bbc93d27a4c7aaab9836a5432b430f1..cc54ed5c03b45315d9765a86ea660bc2e44450e6 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma
@@ -22,7 +22,7 @@ inductive ltpss: nat → nat → relation lenv ≝
 | ltpss_pair : ∀L,I,V. ltpss 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
 | ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
                ltpss 0 e L1 L2 → L2 ⊢ V1 [0, e] ▶* V2 →
-               ltpss 0 (e + 1) (L1. ⓑ{I} V1) L2. ⓑ{I} V2
+               ltpss 0 (e + 1) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
 | ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
                ltpss d e L1 L2 → L2 ⊢ V1 [d, e] ▶* V2 →
                ltpss (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)