X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fexamples%2Fex_snv_eta.ma;h=3a6d5a753236bd428e8c3f2c6ee39d60f59aab2e;hb=e258362c37ec6d9132ec57bd5e4987d148c10799;hp=2320cb5bd88592d8bfdfcae103e2451b489eb03d;hpb=5a35a42e23b2f343f0241eeb6648bf05f31720db;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma
index 2320cb5bd..3a6d5a753 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma
@@ -21,11 +21,11 @@ include "basic_2/dynamic/snv.ma".
 (* extended validity of a closure, last arg of snv_appl > 1 *)
 lemma snv_extended: ∀h,g,a,G,L,k. ⦃G, L.ⓛ⋆k.ⓛⓛ{a}⋆k.⋆k.ⓛ#0⦄ ⊢ ⓐ#2.#0 ¡[h, g].
 #h #g #a #G #L #k elim (deg_total h g k)
-#l #Hl @(snv_appl … a … (⋆k) … (⋆k) (0+1+1))
+#d #Hd @(snv_appl … a … (⋆k) … (⋆k) (0+1+1))
 [ /4 width=5 by snv_lref, drop_drop_lt/
 | /4 width=13 by snv_bind, snv_lref/
 | /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/
-| @(lstas_scpds … (l+1+1))
+| @(lstas_scpds … (d+1+1))
   /5 width=11 by lstas_bind, lstas_succ, da_bind, da_ldec, da_sort, lift_bind/
 ]
 qed.
@@ -33,19 +33,19 @@ qed.
 (* restricted validity of the η-expanded closure, last arg of snv_appl = 1 **)
 lemma snv_restricted: ∀h,g,a,G,L,k. ⦃G, L.ⓛ⋆k.ⓛⓛ{a}⋆k.⋆k.ⓛⓛ{a}⋆k.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ¡[h, g].
 #h #g #a #G #L #k elim (deg_total h g k)
-#l #Hl @(snv_appl … a … (⋆k) … (ⓐ#0.#2) (0+1))
+#d #Hd @(snv_appl … a … (⋆k) … (ⓐ#0.#2) (0+1))
 [ /4 width=5 by snv_lref, drop_drop_lt/
 | @snv_lref [4: // |1,2,3: skip ]
   @snv_bind //
   @(snv_appl … a … (⋆k) … (⋆k) (0+1))
   [ @snv_lref [4: // |1,2,3: skip ] //
   | @snv_lref [4: /2 width=1 by drop_drop_lt/ |1,2,3: skip ] @snv_bind //
-  | @(lstas_scpds … (l+1)) /3 width=6 by da_sort, da_ldec, lstas_succ/
-  | @(lstas_scpds … (l+1)) /3 width=8 by lstas_succ, lstas_bind, drop_drop, lift_bind/
+  | @(lstas_scpds … (d+1)) /3 width=6 by da_sort, da_ldec, lstas_succ/
+  | @(lstas_scpds … (d+1)) /3 width=8 by lstas_succ, lstas_bind, drop_drop, lift_bind/
     @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ] /3 width=1 by da_sort, da_bind/
   ]
 | /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/
-| @(lstas_scpds … (l+1+1)) //
+| @(lstas_scpds … (d+1+1)) //
   [ @da_ldec [3: // |1,2: skip ]
     @da_bind @da_flat @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ]
     /3 width=1 by da_sort, da_bind/