X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fbasics%2Flist.ma;h=d30ed7dfc2a4833f503224f940b7d37c2a866392;hb=63047f8ff8ef477ac32939985b0b41b70e918054;hp=92eddc705b642fb8f984d55c2aea81dc62d68cb1;hpb=35a0b2aaeb0413fedbe7de94973167c98222e30e;p=helm.git

diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma
index 92eddc705..d30ed7dfc 100644
--- a/helm/software/matita/nlibrary/basics/list.ma
+++ b/helm/software/matita/nlibrary/basics/list.ma
@@ -39,7 +39,7 @@ ndefinition not_nil: ∀A:Type.list A → Prop ≝
 
 ntheorem nil_cons:
   ∀A:Type.∀l:list A.∀a:A. a::l ≠ [].
-  #A; #l; #a; #Heq; nchange with (not_nil ? (a::l));
+  #A; #l; #a; napply nmk; #Heq; nchange with (not_nil ? (a::l));
   nrewrite > Heq; //;
 nqed.