- the confluence of context-senstitive parallel reduction (cpr) is closed!

[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 df96372befe0006a2e57f34b28c9ff7fdbf96faf..d72b6c4cb3f355c7bb1381182451c667a2610134 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
@@ -12,23 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic-2/grammar/cl_weight.ma".
+include "Basic-2/grammar/lenv.ma".
 
 (* SHIFT OF A CLOSURE *******************************************************)
 
 let rec shift L T on L ≝ match L with
-[ LSort       ⇒ T
+[ LAtom       ⇒ T
 | LPair L I V ⇒ shift L (𝕓{I} V. T)
 ].
 
 interpretation "shift (closure)" 'Append L T = (shift L T).
-
-(* Basic properties *********************************************************)
-
-lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T].
-#L elim L //
-#K #I #V #IHL #T
-@transitive_le [3: @IHL |2: /2/ | skip ]
-qed.
-
-