diff --git a/test.v b/test.v
index ba48336..a16fd94 100644
--- a/test.v
+++ b/test.v
@@ -80,7 +80,19 @@ Show Proof.
 Qed.  
 End sec_absu_2ismul3.
 
-
+Section vect. 
+  Variable A : Type. 
+  Inductive vector : nat -> Type :=
+    | nil : vector 0
+    | cons : forall n, A -> vector n -> vector (S n). 
+  
+  
+  Goal forall v : vector 0, v = nil. 
+  intros. 
+  Fail invert v. 
+  Abort. 
+End vect. 
+  
 
 Inductive tm : Type :=
   | const : nat -> tm