--- a/list-nat.agda	Fri Jul 12 12:24:29 2013 +0900
+++ b/list-nat.agda	Fri Jul 12 12:28:14 2013 +0900
@@ -38,7 +38,7 @@
 eq-cons :  ∀{n} {A : Set n} {x y : List A} ( a : A ) -> x ==  y -> ( a :: x ) == ( a :: y )
 eq-cons a z = cong1 ( \x -> ( a :: x) ) z
 
-trans-list :  ∀{n} {A : Set n} {x y z : List A} { a : A } -> x ==  y -> y == z -> x == z
+trans-list :  ∀{n} {A : Set n} {x y z : List A}  -> x ==  y -> y == z -> x == z
 trans-list reflection reflection = reflection
 
 
@@ -58,7 +58,7 @@
 list-assoc  (x :: xs)  ys zs = eq-cons x ( list-assoc xs ys zs )
 
 
-module ==-Reasoning {n} (A : Set n) where
+module ==-Reasoning {n} (A : Set n ) where
 
   infixr  2 _∎
   infixr 2 _==⟨_⟩_
@@ -77,14 +77,14 @@
             x == y  → y IsRelatedTo z → x IsRelatedTo z
   _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list x≈y y≈z)
 
-  _∎ : ∀ {a} {A1 : Set a} (x : List A ) → x IsRelatedTo x
+  _∎ : (x : List A ) → x IsRelatedTo x
   _∎ _ = relTo reflection
 
 lemma11 : ∀{n} (A : Set n) ( x : List A ) -> x == x
 lemma11 A x =  let open ==-Reasoning A in
      begin x ∎
       
-++-assoc : (L : Set) ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
+++-assoc : ∀{n} (L : Set n) ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
 ++-assoc A [] ys zs = let open ==-Reasoning A in
   begin -- to prove ([] ++ ys) ++ zs  == [] ++ (ys ++ zs)
    ( [] ++ ys ) ++ zs