λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / append_length.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma
index 1945bac9f0a9890126a5b1929b652099e628bb0a..a0906800cef796ac1e170bb89dc1cd48cc5019bf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma
@@ -102,7 +102,7 @@ qed-.
 (* Basic eliminators ********************************************************)
 
 (* Basic_1: was: c_tail_ind *)
-(* Basic_2A1: was: lenv_ind_alt *) 
+(* Basic_2A1: was: lenv_ind_alt *)
 lemma lenv_ind_tail: ∀Q:predicate lenv.
                      Q (⋆) → (∀I,L. Q L → Q (ⓘ{I}.L)) → ∀L. Q L.
 #Q #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * //