# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1397633185 -32400
# Node ID 36d0732d28e5f67a3f28ff7aa9d695bcd1601b16
# Parent  46fce75667cb07902a73225c37ffe601b7ce5de0
Add comment for lemma-list-nil-cons

diff -r 46fce75667cb -r 36d0732d28e5 systemF.agda
--- a/systemF.agda	Tue Apr 15 17:42:56 2014 +0900
+++ b/systemF.agda	Wed Apr 16 16:26:25 2014 +0900
@@ -161,11 +161,16 @@
 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
 
+-- cannot proove gerenal list ...?
+
 --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
 
-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 for concrete list. has yellow.
 
-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
+--elem2-list : {l ll : Level} {U : Set l} {u1 u2 : U} -> List {l} {ll} U
+--elem2-list {l} {ll} {U} {u1} {u2} = cons u1 (cons u2 nil)
+
+--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}) elem2-list) ≡ elem2-list
+--lemma-list-nil-cons-val = refl
\ No newline at end of file