diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean
index 6404c2d53d..27cce47728 100644
--- a/hott/hit/trunc.hlean
+++ b/hott/hit/trunc.hlean
@@ -104,13 +104,13 @@ namespace trunc
   /- Propositional truncation -/
 
   -- should this live in hprop?
-  definition merely [reducible] (A : Type) : hprop := trunctype.mk (trunc -1 A) _
+  definition merely [reducible] [constructor] (A : Type) : hprop := trunctype.mk (trunc -1 A) _
 
   notation `||`:max A `||`:0 := merely A
   notation `∥`:max A `∥`:0   := merely A
 
-  definition Exists [reducible] (P : X → Type) : hprop := ∥ sigma P ∥
-  definition or [reducible] (A B : Type) : hprop := ∥ A ⊎ B ∥
+  definition Exists [reducible] [constructor] (P : X → Type) : hprop := ∥ sigma P ∥
+  definition or [reducible] [constructor] (A B : Type) : hprop := ∥ A ⊎ B ∥
 
   notation `exists` binders `,` r:(scoped P, Exists P) := r
   notation `∃` binders `,` r:(scoped P, Exists P) := r
diff --git a/hott/types/list.hlean b/hott/types/list.hlean
index e09ac7cd62..ab58630932 100644
--- a/hott/types/list.hlean
+++ b/hott/types/list.hlean
@@ -113,6 +113,14 @@ theorem length_concat (a : T) : ∀ (l : list T), length (concat a l) = length l
 | []      := rfl
 | (x::xs) := by rewrite [concat_cons, *length_cons, length_concat]
 
+theorem concat_append (a : T) : ∀ (l₁ l₂ : list T), concat a l₁ ++ l₂ = l₁ ++ a :: l₂
+| []      := λl₂, rfl
+| (x::xs) := λl₂, begin rewrite [concat_cons,append_cons, concat_append] end
+
+theorem append_concat (a : T)  : ∀(l₁ l₂ : list T), l₁ ++ concat a l₂ = concat a (l₁ ++ l₂)
+| []      := λl₂, rfl
+| (x::xs) := λl₂, begin rewrite [+append_cons, concat_cons, append_concat] end
+
 /- last -/
 
 definition last : Π l : list T, l ≠ [] → T
@@ -746,10 +754,18 @@ theorem map_nil (f : A → B) : map f [] = [] := idp
 
 theorem map_cons (f : A → B) (a : A) (l : list A) : map f (a :: l) = f a :: map f l := idp
 
+lemma map_concat (f : A → B) (a : A) : Πl, map f (concat a l) = concat (f a) (map f l)
+| nil    := rfl
+| (b::l) := begin rewrite [concat_cons, +map_cons, concat_cons, map_concat] end
+
 lemma map_append (f : A → B) : Π l₁ l₂, map f (l₁++l₂) = (map f l₁)++(map f l₂)
 | nil    := take l, rfl
 | (a::l) := take l', begin rewrite [append_cons, *map_cons, append_cons, map_append] end
 
+lemma map_reverse (f : A → B) : Πl, map f (reverse l) = reverse (map f l)
+| nil    := rfl
+| (b::l) := begin rewrite [reverse_cons, +map_cons, reverse_cons, map_concat, map_reverse] end
+
 lemma map_singleton (f : A → B) (a : A) : map f [a] = [f a] := rfl
 
 theorem map_id : Π l : list A, map id l = l
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index add6e8a9f2..66b92f12ba 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -112,6 +112,14 @@ theorem length_concat [simp] (a : T) : ∀ (l : list T), length (concat a l) = l
 | []      := rfl
 | (x::xs) := by rewrite [concat_cons, *length_cons, length_concat]
 
+theorem concat_append (a : T) : ∀ (l₁ l₂ : list T), concat a l₁ ++ l₂ = l₁ ++ a :: l₂
+| []      := λl₂, rfl
+| (x::xs) := λl₂, begin rewrite [concat_cons,append_cons, concat_append] end
+
+theorem append_concat (a : T)  : ∀(l₁ l₂ : list T), l₁ ++ concat a l₂ = concat a (l₁ ++ l₂)
+| []      := λl₂, rfl
+| (x::xs) := λl₂, begin rewrite [+append_cons, concat_cons, append_concat] end
+
 /- last -/
 
 definition last : Π l : list T, l ≠ [] → T
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index bd5ae26d49..b4ebdb4fb2 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -19,10 +19,18 @@ theorem map_nil (f : A → B) : map f [] = []
 
 theorem map_cons (f : A → B) (a : A) (l : list A) : map f (a :: l) = f a :: map f l
 
+lemma map_concat (f : A → B) (a : A) : Πl, map f (concat a l) = concat (f a) (map f l)
+| nil    := rfl
+| (b::l) := begin rewrite [concat_cons, +map_cons, concat_cons, map_concat] end
+
 lemma map_append (f : A → B) : ∀ l₁ l₂, map f (l₁++l₂) = (map f l₁)++(map f l₂)
 | nil    := take l, rfl
 | (a::l) := take l', begin rewrite [append_cons, *map_cons, append_cons, map_append] end
 
+lemma map_reverse (f : A → B) : Πl, map f (reverse l) = reverse (map f l)
+| nil    := rfl
+| (b::l) := begin rewrite [reverse_cons, +map_cons, reverse_cons, map_concat, map_reverse] end
+
 lemma map_singleton (f : A → B) (a : A) : map f [a] = [f a] := rfl
 
 theorem map_id [simp] : ∀ l : list A, map id l = l