]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
some renaming and reordering of variables
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpxs.ma
index 734529a9e4599c5af71bb5f9f60309add20daf13..037113f24082ad5bb7c583564e6161e8365e7a20 100644 (file)
@@ -71,7 +71,7 @@ lemma cpxs_sort: ∀h,o,G,L,s,d1. deg h o s d1 →
 @(cpxs_strap1 … (⋆(iter d2 ℕ (next h) s)))
 [ /3 width=3 by lt_to_le/
 | @(cpx_st … (d1-d2-1)) <plus_minus_k_k
-  /2 width=1 by deg_iter, monotonic_le_minus_r/
+  /2 width=1 by deg_iter, monotonic_le_minus_c/
 ]
 qed.