X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fexamples%2Fex_cpr_omega.ma;h=ad4d40bb95af9104f66d6fb7edee521fff82f974;hb=b4b5f03ffca4f250a1dc02f277b70e4f33ac8a9b;hp=ef27dfa48f0c2e7bc223a56ec6b251c59ff58459;hpb=43282d3750af8831c8100c60d75c56fdfb7ff3c9;p=helm.git

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 ef27dfa48..ad4d40bb9 100644
--- 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,17 +26,17 @@ 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,k. ⬆[l, k] W1 ≡ W2 →
+                  ⬆[l, k] (Delta W1) ≡ (Delta W2).
 /4 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed.
 
 (* Main properties **********************************************************)
 
-theorem cpr_Omega_12: ∀W. ⦃⋆, ⋆⦄ ⊢ Omega1 W ➡ Omega2 W.
+theorem cpr_Omega_12: ∀G,L,W. ⦃G, L⦄ ⊢ Omega1 W ➡ Omega2 W.
 /2 width=1 by cpr_beta/ qed.
 
-theorem cpr_Omega_21: ∀W. ⦃⋆, ⋆⦄ ⊢ Omega2 W ➡ Omega1 W.
-#W1 elim (lift_total W1 0 1) #W2 #HW12
+theorem cpr_Omega_21: ∀G,L,W. ⦃G, L⦄ ⊢ Omega2 W ➡ Omega1 W.
+#G #L #W1 elim (lift_total W1 0 1) #W2 #HW12
 @(cpr_zeta … (Omega1 W2)) /3 width=1 by Delta_lift, lift_flat/
 @cpr_flat @(cpr_delta … (Delta W1) ? 0)
 [3,5,8,10: /2 width=2 by Delta_lift/ |4,9: /2 width=1 by cpr_eps/ |*: skip ]