X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpms_teqx_conf.ma;h=24a56092c849864dd191d8f5690b65a74d9437c1;hp=3271b4e11934081415831173bd181a20b6ac6081;hb=3c7b4071a9ac096b02334c1d47468776b948e2de;hpb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx_conf.ma
index 3271b4e11..24a56092c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx_conf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx_conf.ma
@@ -20,8 +20,8 @@ include "basic_2/dynamic/cnv_cpms_teqx.ma".
 (* Sub confluence propery with restricted rt-transition for terms ***********)
 
 fact cnv_cpms_teqx_strip_lpr_aux (h) (a) (G0) (L0) (T0):
-     (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) →
-     (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) →
+     (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) →
+     (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) →
      ∀n1,T1. ❪G0,L0❫ ⊢ T0 ➡*[h,n1] T1 → ❪G0,L0❫ ⊢ T0 ![h,a] → T0 ≛ T1 →
      ∀n2,T2. ❪G0,L0❫ ⊢ T0 ➡[h,n2] T2 → T0 ≛ T2 →
      ∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 →
@@ -45,8 +45,8 @@ fact cnv_cpms_teqx_strip_lpr_aux (h) (a) (G0) (L0) (T0):
 qed-.
 
 fact cnv_cpms_teqx_conf_lpr_aux (h) (a) (G0) (L0) (T0):
-     (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) →
-     (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) →
+     (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) →
+     (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) →
      ∀n1,T1. ❪G0,L0❫ ⊢ T0 ➡*[h,n1] T1 → ❪G0,L0❫ ⊢ T0 ![h,a] → T0 ≛ T1 →
      ∀n2,T2. ❪G0,L0❫ ⊢ T0 ➡*[h,n2] T2 → T0 ≛ T2 →
      ∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 →