More stuff integrated from CerCo on sigma types (that are now a record)

[helm.git] / matita / matita / lib / basics / lists / list.ma

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 01766b9eceaaa6fe032c5cd4afd8f4ced07e71bc..fa9e8bfee3c32290ccf54dcef5f7faca56a53c5b 100644 (file)
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -117,7 +117,7 @@ theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
 match l1 with
   [ nil ⇒ nil ?
-  | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
+  | cons a tl ⇒ (map ??(mk_Sig ?? a) (g a)) @ dprodl A f tl g
   ].
 
 (**************************** length ******************************)