update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / grammar / lenv_append.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma
index ab90ddf298c9d7dee96e8d2d81108ba21f781200..c7d7ac9ca860277e4cb24d3101fa6def804baf81 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma
@@ -85,7 +85,7 @@ qed-.
 lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 →
                                 ∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K.
 #d @(nat_ind_plus … d) -d
-[ #L #H 
+[ #L #H
   elim (length_inv_pos_dx … H) -H #I #K #V #H
   >(length_inv_zero_dx … H) -H #H destruct
   @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (**) (* /3/ does not work *)
@@ -98,7 +98,7 @@ qed-.
 
 (* Basic_eliminators ********************************************************)
 
-fact lenv_ind_dx_aux: ∀R:predicate lenv. R ⋆ →
+fact lenv_ind_dx_aux: ∀R:predicate lenv. R (⋆) →
                       (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) →
                       ∀d,L. |L| = d → R L.
 #R #Hatom #Hpair #d @(nat_ind_plus … d) -d
@@ -108,7 +108,7 @@ fact lenv_ind_dx_aux: ∀R:predicate lenv. R ⋆ →
 ]
 qed-.
 
-lemma lenv_ind_dx: ∀R:predicate lenv. R ⋆ →
+lemma lenv_ind_dx: ∀R:predicate lenv. R (⋆) →
                    (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) →
                    ∀L. R L.
 /3 width=2 by lenv_ind_dx_aux/ qed-.