X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fexamples%2Fex_fpbg_refl.ma;h=fbc2bd7cd1a117058e4a9f1a37245314371d468c;hb=c60524dec7ace912c416a90d6b926bee8553250b;hp=a0f03d62b4ce1412018d03c935eded8c23ba329f;hpb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_fpbg_refl.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_fpbg_refl.ma
index a0f03d62b..fbc2bd7cd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_fpbg_refl.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_fpbg_refl.ma
@@ -28,8 +28,8 @@ definition ApplOmega3: term → nat → term ≝ λW,k. ⓐ⋆k.(ApplOmega1 W k)
 
 (* Basic properties *********************************************************)
 
-lemma ApplDelta_lift: ∀W1,W2,k,d,e. ⬆[d, e] W1 ≡ W2 →
-                      ⬆[d, e] (ApplDelta W1 k) ≡ (ApplDelta W2 k).
+lemma ApplDelta_lift: ∀W1,W2,k,l,m. ⬆[l, m] W1 ≡ W2 →
+                      ⬆[l, m] (ApplDelta W1 k) ≡ (ApplDelta W2 k).
 /5 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed.
 
 lemma cpr_ApplOmega_12: ∀G,L,W,k. ⦃G, L⦄ ⊢ ApplOmega1 W k ➡ ApplOmega2 W k.