milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_cpmuwe.ma

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 0113889427cc8e1e58049e1d9c8d5ce81bbb4b75..9ba812a95b8a7dac26ebdaf034215bd5c6d64508 100644 (file)
--- 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):