X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Ffpbq.ma;h=3e3472135b3c4a9ad727cfe5b86c0cd83984f555;hp=3175d6556775e3200a20571fd44c90c0d16b68c0;hb=ca7327c20c6031829fade8bb84a3a1bb66113f54;hpb=25c634037771dff0138e5e8e3d4378183ff49b86

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma
index 3175d6556..3e3472135 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma
@@ -37,10 +37,10 @@ lemma fpbq_refl (h): tri_reflexive … (fpbq h).
 /2 width=1 by fpbq_cpx/ qed.
 
 (* Basic_2A1: includes: cpr_fpbq *)
-lemma cpm_fpbq (n) (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[n,h] T2 → ❪G,L,T1❫ ≽[h] ❪G,L,T2❫.
+lemma cpm_fpbq (h) (n) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 → ❪G,L,T1❫ ≽[h] ❪G,L,T2❫.
 /3 width=2 by fpbq_cpx, cpm_fwd_cpx/ qed.
 
-lemma lpr_fpbq (h) (G) (T): ∀L1,L2. ❪G,L1❫ ⊢ ➡[h] L2 → ❪G,L1,T❫ ≽[h] ❪G,L2,T❫.
+lemma lpr_fpbq (h) (G) (T): ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L1,T❫ ≽[h] ❪G,L2,T❫.
 /3 width=1 by fpbq_lpx, lpr_fwd_lpx/ qed.
 
 (* Basic_2A1: removed theorems 2: