- some renaming according to the written version of basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / examples / ex_cpr_omega.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
index 72869603d9b0abebb5c6a656e36bd3cd75363042..68166c915850d2d9604fe022f04a94e574373490 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
@@ -26,8 +26,8 @@ definition Omega2: term → term ≝ λW. +ⓓⓝW.(Delta W).ⓐ#0.#0.
 
 (* Basic properties *********************************************************)
 
-lemma Delta_lift: ∀W1,W2,d,e. ⬆[d, e] W1 ≡ W2 →
-                  ⬆[d, e] (Delta W1) ≡ (Delta W2).
+lemma Delta_lift: ∀W1,W2,l,m. ⬆[l, m] W1 ≡ W2 →
+                  ⬆[l, m] (Delta W1) ≡ (Delta W2).
 /4 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed.
 
 (* Main properties **********************************************************)