# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1397551376 -32400
# Node ID 46fce75667cb07902a73225c37ffe601b7ce5de0
# Parent  1fbfc92d76b514fdda83b61f7a7ce490b0be97c7
Retry prove lemma-list-nil-cons. but not finished.

diff -r 1fbfc92d76b5 -r 46fce75667cb systemF.agda
--- a/systemF.agda	Tue Apr 15 17:20:52 2014 +0900
+++ b/systemF.agda	Tue Apr 15 17:42:56 2014 +0900
@@ -161,16 +161,11 @@
 lemma-list-it-cons : {l : Level} {U W : Set l} {u : U} {w : W} {f : U -> W -> W} {t : List U} -> ListIt w f (cons u t) ≡ f u (ListIt w f t)
 lemma-list-it-cons = refl
 
--- apply nil and cons to List U, return same list. but cannot justify type of cons and ListIt.
--- if W = List U, cons has List U -> List (List U) -> (List U)
-
---lemma-list-nil-cons : {l ll : Level} {U : Set ?} {X : Set ?} {t : List U} -> (ListIt {?} {?} {?} {List U} (nil) (cons) t) ≡ t
+--lemma-list-nil-cons : {l ll : Level} {U : Set l} {t : List {l} {ll} U} -> (ListIt {l} {U} {(l ⊔ (suc ll))} {List {l} {ll} U} (nil {l} {U} {ll}) (cons {l} {U} {ll}) t) ≡ t
 --lemma-list-nil-cons = refl
 
--- try concreate variable. has yellow.
+li : {l ll : Level} {U : Set l} {u1 u2 : U} -> List {l} {ll} U
+li {l} {ll} {U} {u1} {u2} = cons u1 (cons u2 nil) 
 
---li : {l ll : Level} {U : Set l} {u1 u2 : U} -> List {l} {ll} U
---li {l} {ll} {U} {u1} {u2} = cons u1 (cons u2 nil) 
-
---lemma-list-nil-cons-val : {l : Level} {U : Set l} -> (ListIt {l} {U} {suc l} {List U} (nil {l} {U}) (cons {l} {U} {l}) li) ≡ li
---lemma-list-nil-cons-val = refl
\ No newline at end of file
+lemma-list-nil-cons-val : {l ll : Level} {U : Set l} -> (ListIt {l} {U} {(l ⊔ (suc ll))} {List {l} {ll} U} (nil {l} {U} {ll}) (cons {l} {U} {ll}) li) ≡ li 
+lemma-list-nil-cons-val = refl
\ No newline at end of file