DEFINITION pr3_gen_appl()
TYPE =
∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Flat Appl) u1 t1) x
→(or3
ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c u1 u2 λ:T.λt2:T.pr3 c t1 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) x
λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c t1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) x
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2)
BODY =
assume c: C
assume u1: T
assume t1: T
assume x: T
suppose H: pr3 c (THead (Flat Appl) u1 t1) x
assume y: T
suppose H0: pr3 c y x
we proceed by induction on H0 to prove
∀x0:T
.∀x1:T
.eq T y (THead (Flat Appl) x0 x1)
→(or3
ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt2:T.pr3 c x1 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) x
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) x
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2)
case pr3_refl : t:T ⇒
the thesis becomes
∀x0:T
.∀x1:T
.∀H1:eq T t (THead (Flat Appl) x0 x1)
.or3
ex3_2 T T λu2:T.λt2:T.eq T t (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt2:T.pr3 c x1 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) t
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
assume x0: T
assume x1: T
suppose H1: eq T t (THead (Flat Appl) x0 x1)
(h1)
by (refl_equal . .)
eq T (THead (Flat Appl) x0 x1) (THead (Flat Appl) x0 x1)
end of h1
(h2) by (pr3_refl . .) we proved pr3 c x0 x0
(h3) by (pr3_refl . .) we proved pr3 c x1 x1
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt2:T.eq T (THead (Flat Appl) x0 x1) (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.pr3 c x1 t2
by (or3_intro0 . . . previous)
we proved
or3
ex3_2
T
T
λu2:T.λt2:T.eq T (THead (Flat Appl) x0 x1) (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.pr3 c x1 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) (THead (Flat Appl) x0 x1)
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T
.λy2:T
.pr3
c
THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)
THead (Flat Appl) x0 x1
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
by (eq_ind_r . . . previous . H1)
we proved
or3
ex3_2 T T λu2:T.λt2:T.eq T t (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt2:T.pr3 c x1 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) t
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
∀x0:T
.∀x1:T
.∀H1:eq T t (THead (Flat Appl) x0 x1)
.or3
ex3_2 T T λu2:T.λt2:T.eq T t (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt2:T.pr3 c x1 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) t
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case pr3_sing : t2:T t3:T H1:pr2 c t3 t2 t4:T H2:pr3 c t2 t4 ⇒
the thesis becomes
∀x0:T
.∀x1:T
.∀H4:eq T t3 (THead (Flat Appl) x0 x1)
.or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
(H3) by induction hypothesis we know
∀x0:T
.∀x1:T
.eq T t2 (THead (Flat Appl) x0 x1)
→(or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2)
assume x0: T
assume x1: T
suppose H4: eq T t3 (THead (Flat Appl) x0 x1)
(H5)
we proceed by induction on H4 to prove pr2 c (THead (Flat Appl) x0 x1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr2 c (THead (Flat Appl) x0 x1) t2
end of H5
(H6)
by (pr2_gen_appl . . . . H5)
or3
ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr2 c x0 u2 λ:T.λt2:T.pr2 c x1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T x1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T t2 (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr2 c x0 u2
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T
.λy2:T.eq T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr2 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr2 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr2 (CHead c (Bind b) y2) z1 z2
end of H6
we proceed by induction on H6 to prove
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case or3_intro0 : H7:ex3_2 T T λu2:T.λt5:T.eq T t2 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr2 c x0 u2 λ:T.λt5:T.pr2 c x1 t5 ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
we proceed by induction on H7 to prove
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case ex3_2_intro : x2:T x3:T H8:eq T t2 (THead (Flat Appl) x2 x3) H9:pr2 c x0 x2 H10:pr2 c x1 x3 ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
(H11)
we proceed by induction on H8 to prove
∀x4:T
.∀x5:T
.eq T (THead (Flat Appl) x2 x3) (THead (Flat Appl) x4 x5)
→(or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x4 u2 λ:T.λt5:T.pr3 c x5 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x4 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x5 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x5 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x4 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀x4:T
.∀x5:T
.eq T (THead (Flat Appl) x2 x3) (THead (Flat Appl) x4 x5)
→(or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x4 u2 λ:T.λt5:T.pr3 c x5 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x4 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x5 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x5 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x4 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2)
end of H11
(H13)
by (refl_equal . .)
we proved eq T (THead (Flat Appl) x2 x3) (THead (Flat Appl) x2 x3)
by (H11 . . previous)
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x2 u2 λ:T.λt5:T.pr3 c x3 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x2 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x3 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x3 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x2 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
end of H13
we proceed by induction on H13 to prove
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case or3_intro0 : H14:ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x2 u2 λ:T.λt5:T.pr3 c x3 t5 ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
we proceed by induction on H14 to prove
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case ex3_2_intro : x4:T x5:T H15:eq T t4 (THead (Flat Appl) x4 x5) H16:pr3 c x2 x4 H17:pr3 c x3 x5 ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
(h1)
by (refl_equal . .)
eq T (THead (Flat Appl) x4 x5) (THead (Flat Appl) x4 x5)
end of h1
(h2)
by (pr3_sing . . . H9 . H16)
pr3 c x0 x4
end of h2
(h3)
by (pr3_sing . . . H10 . H17)
pr3 c x1 x5
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt5:T.eq T (THead (Flat Appl) x4 x5) (THead (Flat Appl) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 c x1 t5
by (or3_intro0 . . . previous)
we proved
or3
ex3_2
T
T
λu2:T.λt5:T.eq T (THead (Flat Appl) x4 x5) (THead (Flat Appl) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) (THead (Flat Appl) x4 x5)
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T
.λy2:T
.pr3
c
THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)
THead (Flat Appl) x4 x5
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
by (eq_ind_r . . . previous . H15)
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case or3_intro1 : H14:ex4_4 T T T T λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4 λ:T.λ:T.λu2:T.λ:T.pr3 c x2 u2 λy1:T.λz1:T.λ:T.λ:T.pr3 c x3 (THead (Bind Abst) y1 z1) λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5) ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
we proceed by induction on H14 to prove
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case ex4_4_intro : x4:T x5:T x6:T x7:T H15:pr3 c (THead (Bind Abbr) x6 x7) t4 H16:pr3 c x2 x6 H17:pr3 c x3 (THead (Bind Abst) x4 x5) H18:∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x5 x7) ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
(h1)
by (pr3_sing . . . H9 . H16)
pr3 c x0 x6
end of h1
(h2)
by (pr3_sing . . . H10 . H17)
pr3 c x1 (THead (Bind Abst) x4 x5)
end of h2
by (ex4_4_intro . . . . . . . . . . . . H15 h1 h2 H18)
we proved
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
by (or3_intro1 . . . previous)
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case or3_intro2 : H14:ex6_6 B T T T T T λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst) λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x3 (THead (Bind b) y1 z1) λb:B.λ:T.λ:T.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4 λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x2 u2 λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2 λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2 ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
we proceed by induction on H14 to prove
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case ex6_6_intro : x4:B x5:T x6:T x7:T x8:T x9:T H15:not (eq B x4 Abst) H16:pr3 c x3 (THead (Bind x4) x5 x6) H17:pr3 c (THead (Bind x4) x9 (THead (Flat Appl) (lift (S O) O x8) x7)) t4 H18:pr3 c x2 x8 H19:pr3 c x5 x9 H20:pr3 (CHead c (Bind x4) x9) x6 x7 ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
(h1)
by (pr3_sing . . . H10 . H16)
pr3 c x1 (THead (Bind x4) x5 x6)
end of h1
(h2)
by (pr3_sing . . . H9 . H18)
pr3 c x0 x8
end of h2
by (ex6_6_intro . . . . . . . . . . . . . . . . . . H15 h1 H17 h2 H19 H20)
we proved
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
by (or3_intro2 . . . previous)
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case or3_intro1 : H7:ex4_4 T T T T λy1:T.λz1:T.λ:T.λ:T.eq T x1 (THead (Bind Abst) y1 z1) λ:T.λ:T.λu2:T.λt5:T.eq T t2 (THead (Bind Abbr) u2 t5) λ:T.λ:T.λu2:T.λ:T.pr2 c x0 u2 λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) z1 t5) ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
we proceed by induction on H7 to prove
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case ex4_4_intro : x2:T x3:T x4:T x5:T H8:eq T x1 (THead (Bind Abst) x2 x3) H9:eq T t2 (THead (Bind Abbr) x4 x5) H10:pr2 c x0 x4 H11:∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x3 x5) ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
(H13)
we proceed by induction on H9 to prove pr3 c (THead (Bind Abbr) x4 x5) t4
case refl_equal : ⇒
the thesis becomes the hypothesis H2
pr3 c (THead (Bind Abbr) x4 x5) t4
end of H13
(h1) by (pr3_pr2 . . . H10) we proved pr3 c x0 x4
(h2)
by (pr3_refl . .)
pr3 c (THead (Bind Abst) x2 x3) (THead (Bind Abst) x2 x3)
end of h2
(h3)
assume b: B
assume u: T
by (H11 . .)
we proved pr2 (CHead c (Bind b) u) x3 x5
by (pr3_pr2 . . . previous)
we proved pr3 (CHead c (Bind b) u) x3 x5
∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x3 x5)
end of h3
by (ex4_4_intro . . . . . . . . . . . . H13 h1 h2 h3)
we proved
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c (THead (Bind Abst) x2 x3) (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
by (or3_intro1 . . . previous)
we proved
or3
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 c (THead (Bind Abst) x2 x3) t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c (THead (Bind Abst) x2 x3) (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c (THead (Bind Abst) x2 x3) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
by (eq_ind_r . . . previous . H8)
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case or3_intro2 : H7:ex6_6 B T T T T T λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst) λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T x1 (THead (Bind b) y1 z1) λb:B.λ:T.λ:T.λz2:T.λu2:T.λy2:T.eq T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr2 c x0 u2 λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr2 c y1 y2 λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr2 (CHead c (Bind b) y2) z1 z2 ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
we proceed by induction on H7 to prove
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
case ex6_6_intro : x2:B x3:T x4:T x5:T x6:T x7:T H8:not (eq B x2 Abst) H9:eq T x1 (THead (Bind x2) x3 x4) H10:eq T t2 (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6) x5)) H11:pr2 c x0 x6 H12:pr2 c x3 x7 H13:pr2 (CHead c (Bind x2) x7) x4 x5 ⇒
the thesis becomes
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
(H15)
we proceed by induction on H10 to prove pr3 c (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6) x5)) t4
case refl_equal : ⇒
the thesis becomes the hypothesis H2
pr3 c (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6) x5)) t4
end of H15
(h1)
by (pr3_refl . .)
pr3 c (THead (Bind x2) x3 x4) (THead (Bind x2) x3 x4)
end of h1
(h2) by (pr3_pr2 . . . H11) we proved pr3 c x0 x6
(h3) by (pr3_pr2 . . . H12) we proved pr3 c x3 x7
(h4)
by (pr3_pr2 . . . H13)
pr3 (CHead c (Bind x2) x7) x4 x5
end of h4
by (ex6_6_intro . . . . . . . . . . . . . . . . . . H8 h1 H15 h2 h3 h4)
we proved
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c (THead (Bind x2) x3 x4) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
by (or3_intro2 . . . previous)
we proved
or3
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 c (THead (Bind x2) x3 x4) t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c (THead (Bind x2) x3 x4) (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c (THead (Bind x2) x3 x4) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
by (eq_ind_r . . . previous . H9)
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
we proved
or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
∀x0:T
.∀x1:T
.∀H4:eq T t3 (THead (Flat Appl) x0 x1)
.or3
ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Flat Appl) u2 t5) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt5:T.pr3 c x1 t5
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt5:T.pr3 c (THead (Bind Abbr) u2 t5) t4
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t5)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
we proved
∀x0:T
.∀x1:T
.eq T y (THead (Flat Appl) x0 x1)
→(or3
ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c x0 u2 λ:T.λt2:T.pr3 c x1 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) x
λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) x
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c x0 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2)
by (unintro . . . previous)
we proved
∀x0:T
.eq T y (THead (Flat Appl) u1 x0)
→(or3
ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c u1 u2 λ:T.λt2:T.pr3 c x0 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) x
λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c x0 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c x0 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) x
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2)
by (unintro . . . previous)
we proved
eq T y (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c u1 u2 λ:T.λt2:T.pr3 c t1 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) x
λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c t1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) x
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2)
we proved
∀y:T
.pr3 c y x
→(eq T y (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c u1 u2 λ:T.λt2:T.pr3 c t1 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) x
λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c t1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) x
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2))
by (insert_eq . . . . previous H)
we proved
or3
ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c u1 u2 λ:T.λt2:T.pr3 c t1 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) x
λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c t1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) x
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
we proved
∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Flat Appl) u1 t1) x
→(or3
ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c u1 u2 λ:T.λt2:T.pr3 c t1 t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) x
λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c t1 (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) x
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2)