{discriminate,injection} => destruct

[helm.git] / helm / software / matita / library / list / list.ma

diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index bb341d245fad82a43657e4e427956968fac8b3c2..9ecfd50e3ff41bf5cf89e6604ea2ca4986cf7e48 100644 (file)
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -44,7 +44,7 @@ theorem nil_cons:
   intros;
   unfold Not;
   intros;
-  discriminate H.
+  destruct H.
 qed.
 
 let rec id_list A (l: list A) on l :=