X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fexamples%2Fex_cnv_eta.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fexamples%2Fex_cnv_eta.ma;h=9539ab94247a6d9e48e629413f8eee5c84055373;hb=bac74b5cff042d37e1abc9c961a6c41094b8a294;hp=c3c6610856bce4f76d4dda81a4bf77d42b2eeafc;hpb=cacd7323994f7621286dbfd93bbf4c50acfbe918;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
index c3c661085..9539ab942 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
@@ -35,12 +35,12 @@ qed.
 lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G,L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![h].
 #h #p #G #L #s
 @(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2))
-[ /2 width=1 by ylt_inj/
+[ //
 | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
 | @cnv_zero
   @cnv_bind //
   @(cnv_appl … 1 p … (⋆s) … (⋆s))
-  [ /2 width=1 by ylt_inj/
+  [ //
   | /2 width=1 by cnv_sort, cnv_zero/
   | /4 width=1 by cnv_sort, cnv_zero, cnv_lref, cnv_bind/
   | /2 width=3 by cpms_ell, lifts_sort/