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=e258362c37ec6d9132ec57bd5e4987d148c10799;hp=a0f03d62b4ce1412018d03c935eded8c23ba329f;hpb=d71ad5c0d52dff8bc4b77216fbcb0b65ecd7d391;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.