X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbg_fqup.ma;h=71451e88698309a1a512ffe9b23f0476d49d7b0f;hb=3c7b4071a9ac096b02334c1d47468776b948e2de;hp=ce02c890aa3a096ad3b30a74ce42bb50d3ad4ff8;hpb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
index ce02c890a..71451e886 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
@@ -17,16 +17,18 @@ include "basic_2/rt_computation/fpbg.ma".
 
 (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
 
-(* Advanced properties with degree-based equivalence for terms **************)
+(* Advanced properties with sort-irrelevant equivalence for terms ***********)
 
-lemma fpbg_tdeq_div: ∀h,o,G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T⦄ →
-                     ∀T2. T2 ≛[h, o] T → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
-/4 width=5 by fpbg_fdeq_trans, tdeq_fdeq, tdeq_sym/ qed-.
+lemma fpbg_teqx_div:
+      ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ > ❪G2,L2,T❫ →
+      ∀T2. T2 ≛ T → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+/4 width=5 by fpbg_feqx_trans, teqx_feqx, teqx_sym/ qed-.
 
 (* Properties with plus-iterated structural successor for closures **********)
 
 (* Note: this is used in the closure proof *)
-lemma fqup_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
+lemma fqup_fpbg:
+      ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
 /3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_intro/
 qed.