- parallel reduction for local environments: we proved the equivalence

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / grammar / cl_shift.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma
index 837b1c670c65cc6726e129056cbccc0e87d51925..bbdc8e7d09555bb6fad776196ffb37464c21922f 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma
@@ -26,7 +26,7 @@ interpretation "shift (closure)" 'Append L T = (shift L T).
 (* Basic properties *********************************************************)
 
 lemma shift_append_assoc: ∀L,K. ∀T:term. (L @@ K) @@ T = L @@ K @@ T.
-#L #K elim K -K normalize //
+#L #K elim K -K // normalize //
 qed.
 
 (* Basic inversion lemmas ***************************************************)