X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Frpx_reqx.ma;h=912adfc516d1cbadd4b6c59d265fd4eae2b5bf8a;hb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;hp=29964b29c6c9dd78868361f7c0a221af37aaa40c;hpb=b2cdc4abd9ac87e39bc51b0d9c38daea179adbd5;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
index 29964b29c..912adfc51 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
@@ -12,13 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/static/reqx_drops.ma".
-include "static_2/static/reqx_fqup.ma".
-include "static_2/static/reqx_reqx.ma".
-include "basic_2/rt_transition/rpx_fsle.ma".
+include "static_2/syntax/teqx.ma".
+include "basic_2/rt_transition/rpx_reqg.ma".
 
 (* EXTENDED PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS **********)
-
+(*
 (* Properties with sort-irrelevant equivalence for local environments *******)
 
 lemma rpx_pair_sn_split (G):
@@ -41,8 +39,8 @@ lemma rpx_bind_dx_split_void (G):
       ∃∃K2. ❪G,K1❫ ⊢ ⬈[ⓑ[p,I]V.T] K2 & K2.ⓧ ≛[T] L2.
 /3 width=5 by rpx_fsge_comp, rex_bind_dx_split_void/ qed-.
 
-lemma rpx_teqx_conf (G): s_r_confluent1 … cdeq (rpx G).
-/2 width=5 by teqx_rex_conf/ qed-.
+lemma rpx_teqx_conf_sn (G): s_r_confluent1 … cdeq (rpx G).
+/2 width=5 by teqx_rex_conf_sn/ qed-.
 
 lemma rpx_teqx_div (G):
       ∀T1,T2. T1 ≛ T2 → ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T2] L2 → ❪G,L1❫ ⊢ ⬈[T1] L2.
@@ -127,12 +125,11 @@ qed-.
 lemma cpx_teqx_conf (G) (L):
       ∀T0:term. ∀T1. ❪G,L❫ ⊢ T0 ⬈ T1 → ∀T2. T0 ≛ T2 → ❪G,L❫ ⊢ T2 ⬈ T1.
 /2 width=7 by cpx_teqx_repl_reqx/ qed-.
-
+*)
 lemma teqx_cpx_trans (G) (L):
-      ∀T2. ∀T0:term. T2 ≛ T0 → ∀T1. ❪G,L❫ ⊢ T0 ⬈ T1 → ❪G,L❫ ⊢ T2 ⬈ T1.
-/3 width=3 by cpx_teqx_conf, teqx_sym/
-qed-.
-
+      ∀T2. ∀T0:term. T2 ≅ T0 → ∀T1. ❪G,L❫ ⊢ T0 ⬈ T1 → ❪G,L❫ ⊢ T2 ⬈ T1.
+/2 width=6 by teqg_cpx_trans/ qed-.
+(*
 lemma teqx_cpx (G) (L):
       ∀T1,T2:term. T1 ≛ T2 → ❪G,L❫ ⊢ T1 ⬈ T2.
 /2 width=3 by teqx_cpx_trans/ qed.
@@ -159,3 +156,4 @@ lemma reqx_rpx_trans (G) (T) (L):
 lemma reqx_rpx (G) (T):
       ∀L1,L2. L1 ≛[T] L2 → ❪G,L1❫ ⊢ ⬈[T] L2.
 /2 width=3 by reqx_rpx_trans/ qed.
+*)