update in basic_2 and apps_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / fpb.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma
index 5b0c68c2a6f563bcf0897e602ad61f5f96294023..3e31edb7e2d1832059e8b87b6b4c86643a74e62e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma
@@ -32,10 +32,10 @@ interpretation
 (* Basic properties *********************************************************)
 
 (* Basic_2A1: includes: cpr_fpb *)
-lemma cpm_fpb (n) (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[n,h] T2 → (T1 ≛ T2 → ⊥) →
+lemma cpm_fpb (h) (n) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 → (T1 ≛ T2 → ⊥) →
                                    ❪G,L,T1❫ ≻[h] ❪G,L,T2❫.
 /3 width=2 by fpb_cpx, cpm_fwd_cpx/ qed.
 
-lemma lpr_fpb (h) (G) (T): ∀L1,L2. ❪G,L1❫ ⊢ ➡[h] L2 → (L1 ≛[T] L2 → ⊥) →
+lemma lpr_fpb (h) (G) (T): ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → (L1 ≛[T] L2 → ⊥) →
                            ❪G,L1,T❫ ≻[h] ❪G,L2,T❫.
 /3 width=1 by fpb_lpx, lpr_fwd_lpx/ qed.