DEFINITION wcpr0_getl_back()
TYPE =
∀c1:C
.∀c2:C
.wcpr0 c2 c1
→∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.getl h c1 (CHead e1 k u1)
→ex3_2 C T λe2:C.λu2:T.getl h c2 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1
BODY =
assume c1: C
assume c2: C
suppose H: wcpr0 c2 c1
we proceed by induction on H to prove
∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.getl h c1 (CHead e1 k u1)
→ex3_2 C T λe2:C.λu2:T.getl h c2 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1
case wcpr0_refl : c:C ⇒
the thesis becomes
∀h:nat
.∀e1:C
.∀u1:T
.∀k:K.∀H0:(getl h c (CHead e1 k u1)).(ex3_2 C T λe2:C.λu2:T.getl h c (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1)
assume h: nat
assume e1: C
assume u1: T
assume k: K
suppose H0: getl h c (CHead e1 k u1)
(h1) by (wcpr0_refl .) we proved wcpr0 e1 e1
(h2) by (pr0_refl .) we proved pr0 u1 u1
by (ex3_2_intro . . . . . . . H0 h1 h2)
we proved ex3_2 C T λe2:C.λu2:T.getl h c (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1
∀h:nat
.∀e1:C
.∀u1:T
.∀k:K.∀H0:(getl h c (CHead e1 k u1)).(ex3_2 C T λe2:C.λu2:T.getl h c (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1)
case wcpr0_comp : c3:C c4:C H0:wcpr0 c3 c4 u1:T u2:T H2:pr0 u1 u2 k:K ⇒
the thesis becomes
∀h:nat
.∀e1:C
.∀u3:T
.∀k0:K
.getl h (CHead c4 k u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.getl h (CHead c3 k u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
(H1) by induction hypothesis we know
∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.getl h c4 (CHead e1 k u1)
→ex3_2 C T λe2:C.λu2:T.getl h c3 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1
assume h: nat
we proceed by induction on h to prove
∀e1:C
.∀u3:T
.∀k0:K
.getl h (CHead c4 k u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.getl h (CHead c3 k u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
case O : ⇒
the thesis becomes
∀e1:C
.∀u0:T
.∀k0:K
.getl O (CHead c4 k u2) (CHead e1 k0 u0)
→ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 k u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
assume e1: C
assume u0: T
assume k0: K
suppose H3: getl O (CHead c4 k u2) (CHead e1 k0 u0)
by (getl_gen_O . . H3)
we proved clear (CHead c4 k u2) (CHead e1 k0 u0)
assume b: B
suppose H4: clear (CHead c4 (Bind b) u2) (CHead e1 k0 u0)
(H5)
by (clear_gen_bind . . . . H4)
we proved eq C (CHead e1 k0 u0) (CHead c4 (Bind b) u2)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead e1 k0 u0 OF CSort ⇒e1 | CHead c ⇒c
<λ:C.C> CASE CHead c4 (Bind b) u2 OF CSort ⇒e1 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒e1 | CHead c ⇒c (CHead e1 k0 u0)
λe:C.<λ:C.C> CASE e OF CSort ⇒e1 | CHead c ⇒c (CHead c4 (Bind b) u2)
end of H5
(h1)
(H6)
by (clear_gen_bind . . . . H4)
we proved eq C (CHead e1 k0 u0) (CHead c4 (Bind b) u2)
by (f_equal . . . . . previous)
we proved
eq
K
<λ:C.K> CASE CHead e1 k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c4 (Bind b) u2 OF CSort ⇒k0 | CHead k1 ⇒k1
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead e1 k0 u0)
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c4 (Bind b) u2)
end of H6
(h1)
(H7)
by (clear_gen_bind . . . . H4)
we proved eq C (CHead e1 k0 u0) (CHead c4 (Bind b) u2)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead e1 k0 u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead c4 (Bind b) u2 OF CSort ⇒u0 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t⇒t (CHead e1 k0 u0)
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t⇒t (CHead c4 (Bind b) u2)
end of H7
suppose H8: eq K k0 (Bind b)
suppose H9: eq C e1 c4
(h1)
by (getl_refl . . .)
we proved getl O (CHead c3 (Bind b) u1) (CHead c3 (Bind b) u1)
by (ex3_2_intro . . . . . . . previous H0 H2)
we proved
ex3_2
C
T
λe2:C.λu3:T.getl O (CHead c3 (Bind b) u1) (CHead e2 (Bind b) u3)
λe2:C.λ:T.wcpr0 e2 c4
λ:C.λu3:T.pr0 u3 u2
by (eq_ind_r . . . previous . H9)
ex3_2
C
T
λe2:C.λu3:T.getl O (CHead c3 (Bind b) u1) (CHead e2 (Bind b) u3)
λe2:C.λ:T.wcpr0 e2 e1
λ:C.λu3:T.pr0 u3 u2
end of h1
(h2)
consider H7
we proved
eq
T
<λ:C.T> CASE CHead e1 k0 u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead c4 (Bind b) u2 OF CSort ⇒u0 | CHead t⇒t
eq T u0 u2
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ex3_2
C
T
λe2:C.λu3:T.getl O (CHead c3 (Bind b) u1) (CHead e2 (Bind b) u3)
λe2:C.λ:T.wcpr0 e2 e1
λ:C.λu3:T.pr0 u3 u0
by (eq_ind_r . . . previous . H8)
we proved ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
eq K k0 (Bind b)
→(eq C e1 c4
→ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0)
end of h1
(h2)
consider H6
we proved
eq
K
<λ:C.K> CASE CHead e1 k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c4 (Bind b) u2 OF CSort ⇒k0 | CHead k1 ⇒k1
eq K k0 (Bind b)
end of h2
by (h1 h2)
eq C e1 c4
→ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
end of h1
(h2)
consider H5
we proved
eq
C
<λ:C.C> CASE CHead e1 k0 u0 OF CSort ⇒e1 | CHead c ⇒c
<λ:C.C> CASE CHead c4 (Bind b) u2 OF CSort ⇒e1 | CHead c ⇒c
eq C e1 c4
end of h2
by (h1 h2)
we proved ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
∀H4:clear (CHead c4 (Bind b) u2) (CHead e1 k0 u0)
.ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
assume f: F
suppose H4: clear (CHead c4 (Flat f) u2) (CHead e1 k0 u0)
(H5)
(h1)
by (drop_refl .)
drop O O c4 c4
end of h1
(h2)
by (clear_gen_flat . . . . H4)
clear c4 (CHead e1 k0 u0)
end of h2
by (getl_intro . . . . h1 h2)
we proved getl O c4 (CHead e1 k0 u0)
by (H1 . . . . previous)
ex3_2 C T λe2:C.λu2:T.getl O c3 (CHead e2 k0 u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u0
end of H5
we proceed by induction on H5 to prove ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
case ex3_2_intro : x0:C x1:T H6:getl O c3 (CHead x0 k0 x1) H7:wcpr0 x0 e1 H8:pr0 x1 u0 ⇒
the thesis becomes ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
by (getl_flat . . . H6 . .)
we proved getl O (CHead c3 (Flat f) u1) (CHead x0 k0 x1)
by (ex3_2_intro . . . . . . . previous H7 H8)
ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
we proved ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
∀H4:clear (CHead c4 (Flat f) u2) (CHead e1 k0 u0)
.ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
by (previous . previous)
we proved ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 k u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
∀e1:C
.∀u0:T
.∀k0:K
.getl O (CHead c4 k u2) (CHead e1 k0 u0)
→ex3_2 C T λe2:C.λu3:T.getl O (CHead c3 k u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
case S ⇒
we need to prove
∀n:nat
.∀e1:C
.∀u3:T
.∀k1:K
.getl n (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.getl n (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u3:T
.∀k1:K
.getl (S n) (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.getl (S n) (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
we proceed by induction on k to prove
∀n:nat
.∀e1:C
.∀u3:T
.∀k1:K
.getl n (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.getl n (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u3:T
.∀k1:K
.getl (S n) (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.getl (S n) (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
case Bind : b:B ⇒
the thesis becomes
∀n:nat
.∀e1:C
.∀u3:T
.∀k0:K
.getl n (CHead c4 (Bind b) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.getl n (CHead c3 (Bind b) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u0:T
.∀k0:K
.∀H4:getl (S n) (CHead c4 (Bind b) u2) (CHead e1 k0 u0)
.ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
assume n: nat
suppose :
∀e1:C
.∀u3:T
.∀k0:K
.getl n (CHead c4 (Bind b) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.getl n (CHead c3 (Bind b) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
assume e1: C
assume u0: T
assume k0: K
suppose H4: getl (S n) (CHead c4 (Bind b) u2) (CHead e1 k0 u0)
(H5)
by (getl_gen_S . . . . . H4)
we proved getl (r (Bind b) n) c4 (CHead e1 k0 u0)
that is equivalent to getl n c4 (CHead e1 k0 u0)
by (H1 . . . . previous)
ex3_2 C T λe2:C.λu2:T.getl n c3 (CHead e2 k0 u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u0
end of H5
we proceed by induction on H5 to prove ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
case ex3_2_intro : x0:C x1:T H6:getl n c3 (CHead x0 k0 x1) H7:wcpr0 x0 e1 H8:pr0 x1 u0 ⇒
the thesis becomes ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
consider H6
we proved getl n c3 (CHead x0 k0 x1)
that is equivalent to getl (r (Bind b) n) c3 (CHead x0 k0 x1)
by (getl_head . . . . previous .)
we proved getl (S n) (CHead c3 (Bind b) u1) (CHead x0 k0 x1)
by (ex3_2_intro . . . . . . . previous H7 H8)
ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
we proved ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
∀n:nat
.∀e1:C
.∀u3:T
.∀k0:K
.getl n (CHead c4 (Bind b) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.getl n (CHead c3 (Bind b) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u0:T
.∀k0:K
.∀H4:getl (S n) (CHead c4 (Bind b) u2) (CHead e1 k0 u0)
.ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
case Flat : f:F ⇒
the thesis becomes
∀n:nat
.∀e1:C
.∀u3:T
.∀k0:K
.getl n (CHead c4 (Flat f) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.getl n (CHead c3 (Flat f) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u0:T
.∀k0:K
.∀H4:getl (S n) (CHead c4 (Flat f) u2) (CHead e1 k0 u0)
.ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
assume n: nat
suppose :
∀e1:C
.∀u3:T
.∀k0:K
.getl n (CHead c4 (Flat f) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.getl n (CHead c3 (Flat f) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
assume e1: C
assume u0: T
assume k0: K
suppose H4: getl (S n) (CHead c4 (Flat f) u2) (CHead e1 k0 u0)
(H5)
by (getl_gen_S . . . . . H4)
we proved getl (r (Flat f) n) c4 (CHead e1 k0 u0)
that is equivalent to getl (S n) c4 (CHead e1 k0 u0)
by (H1 . . . . previous)
ex3_2 C T λe2:C.λu2:T.getl (S n) c3 (CHead e2 k0 u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u0
end of H5
we proceed by induction on H5 to prove ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
case ex3_2_intro : x0:C x1:T H6:getl (S n) c3 (CHead x0 k0 x1) H7:wcpr0 x0 e1 H8:pr0 x1 u0 ⇒
the thesis becomes ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
consider H6
we proved getl (S n) c3 (CHead x0 k0 x1)
that is equivalent to getl (r (Flat f) n) c3 (CHead x0 k0 x1)
by (getl_head . . . . previous .)
we proved getl (S n) (CHead c3 (Flat f) u1) (CHead x0 k0 x1)
by (ex3_2_intro . . . . . . . previous H7 H8)
ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
we proved ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
∀n:nat
.∀e1:C
.∀u3:T
.∀k0:K
.getl n (CHead c4 (Flat f) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.getl n (CHead c3 (Flat f) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u0:T
.∀k0:K
.∀H4:getl (S n) (CHead c4 (Flat f) u2) (CHead e1 k0 u0)
.ex3_2 C T λe2:C.λu3:T.getl (S n) (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
∀n:nat
.∀e1:C
.∀u3:T
.∀k1:K
.getl n (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.getl n (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u3:T
.∀k1:K
.getl (S n) (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.getl (S n) (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
we proved
∀e1:C
.∀u3:T
.∀k0:K
.getl h (CHead c4 k u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.getl h (CHead c3 k u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
∀h:nat
.∀e1:C
.∀u3:T
.∀k0:K
.getl h (CHead c4 k u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.getl h (CHead c3 k u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
we proved
∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.getl h c1 (CHead e1 k u1)
→ex3_2 C T λe2:C.λu2:T.getl h c2 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1
we proved
∀c1:C
.∀c2:C
.wcpr0 c2 c1
→∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.getl h c1 (CHead e1 k u1)
→ex3_2 C T λe2:C.λu2:T.getl h c2 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1