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