- main lemmas about abstract reducibility candidates closed

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / grammar / cl_weight.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
index 22818a9802bf43b3292d2f6b6421ec4bd3b56403..925b84a34aca11d1ee53dda0c76ea3b92b67a2c1 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
@@ -31,7 +31,7 @@ axiom cw_wf_ind: ∀R:lenv→predicate term.
                  ∀L,T. R L T.
 
 (* Basic_1: was: flt_shift *)
-lemma cw_shift: ∀K,I,V,T. #[K. 𝕓{I} V, T] < #[K, 𝕔{I} V. T].
+lemma cw_shift: ∀K,I,V,T. #[K. ⓑ{I} V, T] < #[K, ②{I} V. T].
 normalize //
 qed.