X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpmuwe.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpmuwe.ma;h=9ba812a95b8a7dac26ebdaf034215bd5c6d64508;hb=c0d38a82464481e3c8fd68e4b00d7b9b448df462;hp=0113889427cc8e1e58049e1d9c8d5ce81bbb4b75;hpb=0fea4ed429678c3293027cfe76fdbe15cfa331cb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma
index 011388942..9ba812a95 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma
@@ -18,7 +18,7 @@ include "basic_2/dynamic/cnv_preserve.ma".
 
 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
 
-(* Properties with head evaluation for t-bound rt-transition on terms *******)
+(* Properties with t-unbound whd evaluation on terms ************************)
 
 lemma cnv_cpmuwe_trans (a) (h) (G) (L):
       ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
@@ -29,9 +29,6 @@ lemma cnv_R_cpmuwe_total (a) (h) (G) (L):
       ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃n. R_cpmuwe h G L T1 n.
 /4 width=2 by cnv_fwd_fsb, fsb_inv_csx, R_cpmuwe_total_csx/ qed-.
 
-axiom cnv_R_cpmuwe_dec (a) (h) (G) (L):
-      ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀n. Decidable (R_cpmuwe h G L T n).
-
 (* Main inversions with head evaluation for t-bound rt-transition on terms **)
 
 theorem cnv_cpmuwe_mono (a) (h) (G) (L):