# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1394980405 -25200
# Node ID 29b04e89ebb8135b389ea18b48a9519f8b38f9d3
# Parent  7a3229b32b3cd70927dbf8116664d3cc15b9928d
iota

diff -r 7a3229b32b3c -r 29b04e89ebb8 system-f.agda
--- a/system-f.agda	Sun Mar 16 17:51:55 2014 +0700
+++ b/system-f.agda	Sun Mar 16 21:33:25 2014 +0700
@@ -87,15 +87,13 @@
 ι2 : {U V : Set l} ->  V ->  U + V
 ι2 {U} {V} v = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> y v
 
--- δ's aguments should aware x as raw symbol
+δ : { U V R S : Set l } -> (R -> U) -> (S -> U) -> ( R + S ) -> U
+δ  {U} {V} {R} {S} u v t = t {U} (\(x : R) -> u x) ( \(y : S) -> v y)
 
-δ : { U V R S : Set l } -> U -> U -> ( R + S ) -> U
-δ  {U} {V} {R} {S} u v t = t {U} (\(x : R) -> u ) ( \(y : S) -> v )
-
-lemma11 : { U V R S : Set l } -> (u v : U ) -> (r : R) -> δ  {U} {V} {R} {S} u v ( ι1 r )  ≡ u
+lemma11 : { U V R S : Set l } -> (u : R -> U ) (v : S -> U ) -> (r : R) -> δ  {U} {V} {R} {S} u v ( ι1 r )  ≡ u r
 lemma11 u v r =  refl
 
-lemma12 : { U V R S : Set l } -> (u v : U ) -> (s : S) -> δ  {U} {V} {R} {S} u v ( ι2 s )  ≡ v
+lemma12 : { U V R S : Set l } -> (u : R -> U ) (v : S -> U ) -> (s : S) -> δ  {U} {V} {R} {S} u v ( ι2 s )  ≡ v s
 lemma12 u v s =  refl