x)).(ex_intro2 T (\lambda (t: T).(pr3 c1 t1 t)) (\lambda (t: T).(pr3 c1 t2
t)) x (clear_pr3_trans c2 t1 x H2 c1 H0) (clear_pr3_trans c2 t2 x H3 c1
H0))))) H1))))))).
x)).(ex_intro2 T (\lambda (t: T).(pr3 c1 t1 t)) (\lambda (t: T).(pr3 c1 t2
t)) x (clear_pr3_trans c2 t1 x H2 c1 H0) (clear_pr3_trans c2 t2 x H3 c1
H0))))) H1))))))).
\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t1
t2)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
t2 (pr3_pr2 c t1 t2 H) (pr3_refl c t2))))).
\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t1
t2)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
t2 (pr3_pr2 c t1 t2 H) (pr3_refl c t2))))).
\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t2
t1)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
t1 (pr3_refl c t1) (pr3_pr2 c t2 t1 H))))).
\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t2
t1)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
t1 (pr3_refl c t1) (pr3_pr2 c t2 t1 H))))).
\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr3 c t1
t2)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
t2 H (pr3_refl c t2))))).
\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr3 c t1
t2)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
t2 H (pr3_refl c t2))))).
\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr3 c t2
t1)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
t1 (pr3_refl c t1) H)))).
\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr3 c t2
t1)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
t1 (pr3_refl c t1) H)))).
\lambda (c: C).(\lambda (t1: T).(\lambda (t0: T).(\lambda (H: (pr3 c t1
t0)).(\lambda (t2: T).(\lambda (H0: (pr3 c t2 t0)).(ex_intro2 T (\lambda (t:
T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t)) t0 H H0)))))).
\lambda (c: C).(\lambda (t1: T).(\lambda (t0: T).(\lambda (H: (pr3 c t1
t0)).(\lambda (t2: T).(\lambda (H0: (pr3 c t2 t0)).(ex_intro2 T (\lambda (t:
T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t)) t0 H H0)))))).
theorem pc3_refl:
\forall (c: C).(\forall (t: T).(pc3 c t t))
\def
\lambda (c: C).(\lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr3 c t t0))
(\lambda (t0: T).(pr3 c t t0)) t (pr3_refl c t) (pr3_refl c t))).
theorem pc3_refl:
\forall (c: C).(\forall (t: T).(pc3 c t t))
\def
\lambda (c: C).(\lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr3 c t t0))
(\lambda (t0: T).(pr3 c t t0)) t (pr3_refl c t) (pr3_refl c t))).
T).(pr3 c t2 t)) (pc3 c t2 t1) (\lambda (x: T).(\lambda (H1: (pr3 c t1
x)).(\lambda (H2: (pr3 c t2 x)).(ex_intro2 T (\lambda (t: T).(pr3 c t2 t))
(\lambda (t: T).(pr3 c t1 t)) x H2 H1)))) H0))))).
T).(pr3 c t2 t)) (pc3 c t2 t1) (\lambda (x: T).(\lambda (H1: (pr3 c t1
x)).(\lambda (H2: (pr3 c t2 x)).(ex_intro2 T (\lambda (t: T).(pr3 c t2 t))
(\lambda (t: T).(pr3 c t1 t)) x H2 H1)))) H0))))).
(Flat f) u t1) t)) (\lambda (t: T).(pr3 c (THead (Flat f) u t2) t)) (THead
(Flat f) u x) (pr3_thin_dx c t1 x H1 u f) (pr3_thin_dx c t2 x H2 u f)))))
H0))))))).
(Flat f) u t1) t)) (\lambda (t: T).(pr3 c (THead (Flat f) u t2) t)) (THead
(Flat f) u x) (pr3_thin_dx c t1 x H1 u f) (pr3_thin_dx c t2 x H2 u f)))))
H0))))))).
(\lambda (t0: T).(pr3 c (THead k u2 t) t0)) (THead k x t) (pr3_head_12 c u1 x
H1 k t t (pr3_refl (CHead c k x) t)) (pr3_head_12 c u2 x H2 k t t (pr3_refl
(CHead c k x) t)))))) H0))))))).
(\lambda (t0: T).(pr3 c (THead k u2 t) t0)) (THead k x t) (pr3_head_12 c u1 x
H1 k t t (pr3_refl (CHead c k x) t)) (pr3_head_12 c u2 x H2 k t t (pr3_refl
(CHead c k x) t)))))) H0))))))).
T (\lambda (t: T).(pr3 c (THead k u t1) t)) (\lambda (t: T).(pr3 c (THead k u
t2) t)) (THead k u x) (pr3_head_12 c u u (pr3_refl c u) k t1 x H1)
(pr3_head_12 c u u (pr3_refl c u) k t2 x H2))))) H0))))))).
T (\lambda (t: T).(pr3 c (THead k u t1) t)) (\lambda (t: T).(pr3 c (THead k u
t2) t)) (THead k u x) (pr3_head_12 c u u (pr3_refl c u) k t1 x H1)
(pr3_head_12 c u u (pr3_refl c u) k t2 x H2))))) H0))))))).
t1 t3) (\lambda (x: T).(\lambda (H2: (pr3 c t2 x)).(\lambda (H3: (pr3 c t3
x)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t3 t))
x (pr3_sing c t2 t1 H x H2) H3)))) H1))))))).
t1 t3) (\lambda (x: T).(\lambda (H2: (pr3 c t2 x)).(\lambda (H3: (pr3 c t3
x)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t3 t))
x (pr3_sing c t2 t1 H x H2) H3)))) H1))))))).
(pr3 c x0 x1)).(\lambda (H8: (pr3 c x x1)).(pc3_pr3_t c t1 x1 (pr3_t x0 t1 c
H5 x1 H7) t3 (pr3_t x t3 c H3 x1 H8))))) (pr3_confluence c t2 x0 H6 x H2)))))
H4))))) H1))))))).
(pr3 c x0 x1)).(\lambda (H8: (pr3 c x x1)).(pc3_pr3_t c t1 x1 (pr3_t x0 t1 c
H5 x1 H7) t3 (pr3_t x t3 c H3 x1 H8))))) (pr3_confluence c t2 x0 H6 x H2)))))
H4))))) H1))))))).
\lambda (c: C).(\lambda (t0: T).(\lambda (t1: T).(\lambda (H: (pr2 c t0
t1)).(\lambda (t2: T).(\lambda (H0: (pc3 c t0 t2)).(pc3_t t0 c t1 (pc3_pr2_x
c t1 t0 H) t2 H0)))))).
\lambda (c: C).(\lambda (t0: T).(\lambda (t1: T).(\lambda (H: (pr2 c t0
t1)).(\lambda (t2: T).(\lambda (H0: (pc3 c t0 t2)).(pc3_t t0 c t1 (pc3_pr2_x
c t1 t0 H) t2 H0)))))).
\lambda (c: C).(\lambda (t: T).(\lambda (t1: T).(\lambda (H: (pc3 c t
t1)).(\lambda (t2: T).(\lambda (H0: (pr3 c t t2)).(pc3_t t c t2 (pc3_pr3_x c
t2 t H0) t1 H)))))).
\lambda (c: C).(\lambda (t: T).(\lambda (t1: T).(\lambda (H: (pc3 c t
t1)).(\lambda (t2: T).(\lambda (H0: (pr3 c t t2)).(pc3_t t c t2 (pc3_pr3_x c
t2 t H0) t1 H)))))).
u2)).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pc3
(CHead c k u2) t1 t2)).(pc3_t (THead k u2 t1) c (THead k u1 t1) (pc3_head_1 c
u1 u2 H k t1) (THead k u2 t2) (pc3_head_2 c u2 t1 t2 k H0))))))))).
u2)).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pc3
(CHead c k u2) t1 t2)).(pc3_t (THead k u2 t1) c (THead k u1 t1) (pc3_head_1 c
u1 u2 H k t1) (THead k u2 t2) (pc3_head_2 c u2 t1 t2 k H0))))))))).
u2)).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pc3
(CHead c k u1) t1 t2)).(pc3_t (THead k u1 t2) c (THead k u1 t1) (pc3_head_2 c
u1 t1 t2 k H0) (THead k u2 t2) (pc3_head_1 c u1 u2 H k t2))))))))).
u2)).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pc3
(CHead c k u1) t1 t2)).(pc3_t (THead k u1 t2) c (THead k u1 t1) (pc3_head_2 c
u1 t1 t2 k H0) (THead k u2 t2) (pc3_head_1 c u1 u2 H k t2))))))))).
(pr2_cflat c t3 t (pr2_delta c d u (r (Flat f) i0) H10 t3 t4 H3 t H9) f
u1))))) k IHi (getl_gen_S k c (CHead d (Bind Abbr) u) u2 i0 H8)))))) i H7
H4)))))))))))))) y t1 t2 H1))) H0)))))))).
(pr2_cflat c t3 t (pr2_delta c d u (r (Flat f) i0) H10 t3 t4 H3 t H9) f
u1))))) k IHi (getl_gen_S k c (CHead d (Bind Abbr) u) u2 i0 H8)))))) i H7
H4)))))))))))))) y t1 t2 H1))) H0)))))))).
H12 t4 t5 H6 t6 H11) f t)))) k (getl_gen_S k c0 (CHead d0 (Bind Abbr) u0) t1
i1 H10)))))) i0 H9 H7))))))))))))) y t0 t3 H4))) H3))))))))))))))) c u2 u1
H)))).
H12 t4 t5 H6 t6 H11) f t)))) k (getl_gen_S k c0 (CHead d0 (Bind Abbr) u0) t1
i1 H10)))))) i0 H9 H7))))))))))))) y t0 t3 H4))) H3))))))))))))))) c u2 u1
H)))).
\to (pc3 (CHead c k u1) t0 t4))))).(\lambda (u1: T).(\lambda (H3: (pr2 c u2
u1)).(pc3_t t0 (CHead c k u1) t3 (pc3_pr2_pr2_t c u1 u2 H3 t3 t0 k H0) t4 (H2
u1 H3)))))))))) t1 t2 H)))))).
\to (pc3 (CHead c k u1) t0 t4))))).(\lambda (u1: T).(\lambda (H3: (pr2 c u2
u1)).(pc3_t t0 (CHead c k u1) t3 (pc3_pr2_pr2_t c u1 u2 H3 t3 t0 k H0) t4 (H2
u1 H3)))))))))) t1 t2 H)))))).
(pr3 (CHead c k t1) t4 x)).(pc3_t x (CHead c k t2) t0 (pc3_pr2_pr3_t c t1 t0
x k H5 t2 H0) t4 (pc3_s (CHead c k t2) x t4 (pc3_pr2_pr3_t c t1 t4 x k H6 t2
H0)))))) H4))))))))))))) u2 u1 H)))).
(pr3 (CHead c k t1) t4 x)).(pc3_t x (CHead c k t2) t0 (pc3_pr2_pr3_t c t1 t0
x k H5 t2 H0) t4 (pc3_s (CHead c k t2) x t4 (pc3_pr2_pr3_t c t1 t4 x k H6 t2
H0)))))) H4))))))))))))) u2 u1 H)))).
(H2: (pr3 e t1 x)).(\lambda (H3: (pr3 e t2 x)).(pc3_pr3_t c (lift h d t1)
(lift h d x) (pr3_lift c e h d H t1 x H2) (lift h d t2) (pr3_lift c e h d H
t2 x H3))))) H1))))))))).
(H2: (pr3 e t1 x)).(\lambda (H3: (pr3 e t2 x)).(pc3_pr3_t c (lift h d t1)
(lift h d x) (pr3_lift c e h d H t1 x H2) (lift h d t2) (pr3_lift c e h d H
t2 x H3))))) H1))))))))).
(pc3_pr3_r c (THead (Bind Abst) w (THead (Flat Appl) (TLRef O) (lift (S O) O
(THead (Bind Abst) w u)))) (THead (Bind Abst) w u) (pr3_eta c w u w (pr3_refl
c w))) t (pc3_s c (THead (Bind Abst) w u) t H))))))))).
(pc3_pr3_r c (THead (Bind Abst) w (THead (Flat Appl) (TLRef O) (lift (S O) O
(THead (Bind Abst) w u)))) (THead (Bind Abst) w u) (pr3_eta c w u w (pr3_refl
c w))) t (pc3_s c (THead (Bind Abst) w u) t H))))))))).