finished semantics for termination of match machine

[helm.git] / matita / matita / lib / basics / vectors.ma

diff --git a/matita/matita/lib/basics/vectors.ma b/matita/matita/lib/basics/vectors.ma
index e680e91a7170a48ce231d9c4408f7028f2bbe2e8..a48f04d0fe8dbbfa585262f441fd76a5e78d7c72 100644 (file)
--- a/matita/matita/lib/basics/vectors.ma
+++ b/matita/matita/lib/basics/vectors.ma
@@ -16,6 +16,9 @@ record Vector (A:Type[0]) (n:nat): Type[0] ≝
   len: length ? vec = n
 }.
 
+lemma Vector_of_list ≝ λA,l. 
+  mk_Vector A (|l|) l (refl ??).
+
 lemma Vector_eq : ∀A,n,v1,v2.
   vec A n v1 = vec A n v2 → v1 = v2.
 #A #n * #l1 #H1 * #l2 #H2 #eql1l2 generalize in match H1;