# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1395455506 -25200
# Node ID c4514e0cf0e2b89ea1803729dc981254510ba29b
# Parent  d6eb3520ccf894e8ef1a1115f3fd4a3ca11dc892
no yellow on append example

diff -r d6eb3520ccf8 -r c4514e0cf0e2 system-f.agda
--- a/system-f.agda	Sat Mar 22 09:28:33 2014 +0700
+++ b/system-f.agda	Sat Mar 22 09:31:46 2014 +0700
@@ -206,7 +206,7 @@
 Append : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {_} -> List {l} {U} {X} -> List {l} {U} {_}
 Append {l} {U} {X} x y = \s t -> x (y s t) t
 
-lemma18 : Append l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
+lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {l} {Int {l} {U}} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
 lemma18 = refl
 
 Tree = \{l : Level} -> \{ U X : Set l}  -> X -> ( (U -> X) ->  X ) -> X