Aggiornamento alla negazione.

[helm.git] / helm / software / matita / nlibrary / basics / list.ma

diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma
index 92eddc705b642fb8f984d55c2aea81dc62d68cb1..d30ed7dfc2a4833f503224f940b7d37c2a866392 100644 (file)
--- 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.