T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) x0 x1
(drop_drop (Flat f) n c4 (CHead x0 k0 x1) H6 u2) H7 H8)))))) H5))))))))) k)
h)))))))))) c1 c2 H))).
T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) x0 x1
(drop_drop (Flat f) n c4 (CHead x0 k0 x1) H6 u2) H7 H8)))))) H5))))))))) k)
h)))))))))) c1 c2 H))).
T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) x0 x1
(drop_drop (Flat f) n c3 (CHead x0 k0 x1) H6 u1) H7 H8)))))) H5))))))))) k)
h)))))))))) c2 c1 H))).
T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) x0 x1
(drop_drop (Flat f) n c3 (CHead x0 k0 x1) H6 u1) H7 H8)))))) H5))))))))) k)
h)))))))))) c2 c1 H))).
(\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
(u3: T).(pr0 u0 u3))) x0 x1 (getl_head (Flat f) n c4 (CHead x0 k0 x1) H6 u2)
H7 H8)))))) H5))))))))) k) h)))))))))) c1 c2 H))).
(\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
(u3: T).(pr0 u0 u3))) x0 x1 (getl_head (Flat f) n c4 (CHead x0 k0 x1) H6 u2)
H7 H8)))))) H5))))))))) k) h)))))))))) c1 c2 H))).
(\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
(u3: T).(pr0 u3 u0))) x0 x1 (getl_head (Flat f) n c3 (CHead x0 k0 x1) H6 u1)
H7 H8)))))) H5))))))))) k) h)))))))))) c2 c1 H))).
(\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
(u3: T).(pr0 u3 u0))) x0 x1 (getl_head (Flat f) n c3 (CHead x0 k0 x1) H6 u1)
H7 H8)))))) H5))))))))) k) h)))))))))) c2 c1 H))).