DEFINITION pr0_gen_appl()
TYPE =
∀u1:T
.∀t1:T
.∀x:T
.pr0 (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.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt2:T
.eq T x (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2)
BODY =
assume u1: T
assume t1: T
assume x: T
suppose H: pr0 (THead (Flat Appl) u1 t1) x
assume y: T
suppose H0: pr0 y x
we proceed by induction on H0 to prove
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.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt2:T
.eq T x (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2)
case pr0_refl : t:T ⇒
the thesis becomes
∀H1:eq T t (THead (Flat Appl) u1 t1)
.or3
ex3_2 T T λu2:T.λt2:T.eq T t (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T t (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt2:T
.eq T t (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2
suppose H1: eq T t (THead (Flat Appl) u1 t1)
(H2)
by (f_equal . . . . . H1)
we proved eq T t (THead (Flat Appl) u1 t1)
eq T (λe:T.e t) (λe:T.e (THead (Flat Appl) u1 t1))
end of H2
(h1)
by (refl_equal . .)
eq T (THead (Flat Appl) u1 t1) (THead (Flat Appl) u1 t1)
end of h1
(h2) by (pr0_refl .) we proved pr0 u1 u1
(h3) by (pr0_refl .) we proved pr0 t1 t1
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt2:T.eq T (THead (Flat Appl) u1 t1) (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr0 u1 u2
λ:T.λt2:T.pr0 t1 t2
by (or3_intro0 . . . previous)
we proved
or3
ex3_2
T
T
λu2:T.λt2:T.eq T (THead (Flat Appl) u1 t1) (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr0 u1 u2
λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T (THead (Flat Appl) u1 t1) (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt2:T
.eq
T
THead (Flat Appl) u1 t1
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2)
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2
by (eq_ind_r . . . previous . H2)
we proved
or3
ex3_2 T T λu2:T.λt2:T.eq T t (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T t (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt2:T
.eq T t (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2
∀H1:eq T t (THead (Flat Appl) u1 t1)
.or3
ex3_2 T T λu2:T.λt2:T.eq T t (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T t (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt2:T
.eq T t (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2
case pr0_comp : u0:T u2:T H1:pr0 u0 u2 t0:T t2:T H3:pr0 t0 t2 k:K ⇒
the thesis becomes
∀H5:eq T (THead k u0 t0) (THead (Flat Appl) u1 t1)
.or3
ex3_2 T T λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Flat Appl) u3 t3) λu3:T.λ:T.pr0 u1 u3 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T
.eq
T
THead k u2 t2
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
(H2) by induction hypothesis we know
eq T u0 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu3:T.λt2:T.eq T u2 (THead (Flat Appl) u3 t2) λu3:T.λ:T.pr0 u1 u3 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt2:T.eq T u2 (THead (Bind Abbr) u3 t2)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt2:T.eq T u2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t2))
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2)
(H4) by induction hypothesis we know
eq T t0 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu3:T.λt3:T.eq T t2 (THead (Flat Appl) u3 t3) λu3:T.λ:T.pr0 u1 u3 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T t2 (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T.eq T t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3))
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
suppose H5: eq T (THead k u0 t0) (THead (Flat Appl) u1 t1)
(H6)
by (f_equal . . . . . H5)
we proved
eq
K
<λ:T.K> CASE THead k u0 t0 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K> CASE THead (Flat Appl) u1 t1 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0 (THead k u0 t0)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
THead (Flat Appl) u1 t1
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead k u0 t0 OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t
<λ:T.T> CASE THead (Flat Appl) u1 t1 OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t (THead k u0 t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t
THead (Flat Appl) u1 t1
end of H7
(h1)
(H8)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead k u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
<λ:T.T> CASE THead (Flat Appl) u1 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t (THead k u0 t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
THead (Flat Appl) u1 t1
end of H8
suppose H9: eq T u0 u1
suppose H10: eq K k (Flat Appl)
(H12)
consider H8
we proved
eq
T
<λ:T.T> CASE THead k u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
<λ:T.T> CASE THead (Flat Appl) u1 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
that is equivalent to eq T t0 t1
we proceed by induction on the previous result to prove pr0 t1 t2
case refl_equal : ⇒
the thesis becomes the hypothesis H3
pr0 t1 t2
end of H12
(H14)
we proceed by induction on H9 to prove pr0 u1 u2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr0 u1 u2
end of H14
by (refl_equal . .)
we proved eq T (THead (Flat Appl) u2 t2) (THead (Flat Appl) u2 t2)
by (ex3_2_intro . . . . . . . previous H14 H12)
we proved
ex3_2
T
T
λu3:T.λt3:T.eq T (THead (Flat Appl) u2 t2) (THead (Flat Appl) u3 t3)
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
by (or3_intro0 . . . previous)
we proved
or3
ex3_2
T
T
λu3:T.λt3:T.eq T (THead (Flat Appl) u2 t2) (THead (Flat Appl) u3 t3)
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T (THead (Flat Appl) u2 t2) (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T
.eq
T
THead (Flat Appl) u2 t2
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
by (eq_ind_r . . . previous . H10)
we proved
or3
ex3_2 T T λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Flat Appl) u3 t3) λu3:T.λ:T.pr0 u1 u3 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T
.eq
T
THead k u2 t2
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
eq T u0 u1
→(eq K k (Flat Appl)
→(or3
ex3_2 T T λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Flat Appl) u3 t3) λu3:T.λ:T.pr0 u1 u3 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T
.eq
T
THead k u2 t2
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3))
end of h1
(h2)
consider H7
we proved
eq
T
<λ:T.T> CASE THead k u0 t0 OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t
<λ:T.T> CASE THead (Flat Appl) u1 t1 OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t
eq T u0 u1
end of h2
by (h1 h2)
eq K k (Flat Appl)
→(or3
ex3_2 T T λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Flat Appl) u3 t3) λu3:T.λ:T.pr0 u1 u3 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T
.eq
T
THead k u2 t2
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
end of h1
(h2)
consider H6
we proved
eq
K
<λ:T.K> CASE THead k u0 t0 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K> CASE THead (Flat Appl) u1 t1 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
eq K k (Flat Appl)
end of h2
by (h1 h2)
we proved
or3
ex3_2 T T λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Flat Appl) u3 t3) λu3:T.λ:T.pr0 u1 u3 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T
.eq
T
THead k u2 t2
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
∀H5:eq T (THead k u0 t0) (THead (Flat Appl) u1 t1)
.or3
ex3_2 T T λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Flat Appl) u3 t3) λu3:T.λ:T.pr0 u1 u3 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T (THead k u2 t2) (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T
.eq
T
THead k u2 t2
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
case pr0_beta : u:T v1:T v2:T H1:pr0 v1 v2 t0:T t2:T H3:pr0 t0 t2 ⇒
the thesis becomes
∀H5:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u t0)
THead (Flat Appl) u1 t1
.or3
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Flat Appl) u2 t3)
λu2:T.λ:T.pr0 u1 u2
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt3:T
.eq
T
THead (Bind Abbr) v2 t2
THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t3)
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
(H2) by induction hypothesis we know
eq T v1 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu2:T.λt2:T.eq T v2 (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T v2 (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt2:T.eq T v2 (THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2)
(H4) by induction hypothesis we know
eq T t0 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt3:T.eq T t2 (THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
suppose H5:
eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u t0)
THead (Flat Appl) u1 t1
(H6)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u t0) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t ⇒t
<λ:T.T> CASE THead (Flat Appl) u1 t1 OF TSort ⇒v1 | TLRef ⇒v1 | THead t ⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t ⇒t
THead (Flat Appl) v1 (THead (Bind Abst) u t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t ⇒t
THead (Flat Appl) u1 t1
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u t0) OF
TSort ⇒THead (Bind Abst) u t0
| TLRef ⇒THead (Bind Abst) u t0
| THead t⇒t
<λ:T.T>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒THead (Bind Abst) u t0
| TLRef ⇒THead (Bind Abst) u t0
| THead t⇒t
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind Abst) u t0
| TLRef ⇒THead (Bind Abst) u t0
| THead t⇒t
THead (Flat Appl) v1 (THead (Bind Abst) u t0)
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind Abst) u t0
| TLRef ⇒THead (Bind Abst) u t0
| THead t⇒t
THead (Flat Appl) u1 t1
end of H7
suppose H8: eq T v1 u1
(H9)
we proceed by induction on H8 to prove
eq T u1 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu2:T.λt3:T.eq T v2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T v2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt3:T.eq T v2 (THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
eq T u1 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu2:T.λt3:T.eq T v2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T v2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt3:T.eq T v2 (THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
end of H9
(H10)
we proceed by induction on H8 to prove pr0 u1 v2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr0 u1 v2
end of H10
consider H7
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u t0) OF
TSort ⇒THead (Bind Abst) u t0
| TLRef ⇒THead (Bind Abst) u t0
| THead t⇒t
<λ:T.T>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒THead (Bind Abst) u t0
| TLRef ⇒THead (Bind Abst) u t0
| THead t⇒t
that is equivalent to eq T (THead (Bind Abst) u t0) t1
we proceed by induction on the previous result to prove
or3
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Flat Appl) u2 t3)
λu2:T.λ:T.pr0 u1 u2
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt3:T
.eq
T
THead (Bind Abbr) v2 t2
THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t3)
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
case refl_equal : ⇒
the thesis becomes
or3
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Flat Appl) u2 t3)
λu2:T.λ:T.pr0 u1 u2
λ:T.λt3:T.pr0 (THead (Bind Abst) u t0) t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 (THead (Bind Abst) u t0) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt3:T
.eq
T
THead (Bind Abbr) v2 t2
THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t3)
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
(h1)
by (refl_equal . .)
eq T (THead (Bind Abst) u t0) (THead (Bind Abst) u t0)
end of h1
(h2)
by (refl_equal . .)
eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) v2 t2)
end of h2
by (ex4_4_intro . . . . . . . . . . . . h1 h2 H10 H3)
we proved
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
by (or3_intro1 . . . previous)
or3
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Flat Appl) u2 t3)
λu2:T.λ:T.pr0 u1 u2
λ:T.λt3:T.pr0 (THead (Bind Abst) u t0) t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 (THead (Bind Abst) u t0) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt3:T
.eq
T
THead (Bind Abbr) v2 t2
THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t3)
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
we proved
or3
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Flat Appl) u2 t3)
λu2:T.λ:T.pr0 u1 u2
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt3:T
.eq
T
THead (Bind Abbr) v2 t2
THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t3)
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
eq T v1 u1
→(or3
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Flat Appl) u2 t3)
λu2:T.λ:T.pr0 u1 u2
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt3:T
.eq
T
THead (Bind Abbr) v2 t2
THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t3)
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
end of h1
(h2)
consider H6
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u t0) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t ⇒t
<λ:T.T> CASE THead (Flat Appl) u1 t1 OF TSort ⇒v1 | TLRef ⇒v1 | THead t ⇒t
eq T v1 u1
end of h2
by (h1 h2)
we proved
or3
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Flat Appl) u2 t3)
λu2:T.λ:T.pr0 u1 u2
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt3:T
.eq
T
THead (Bind Abbr) v2 t2
THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t3)
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
∀H5:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u t0)
THead (Flat Appl) u1 t1
.or3
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Flat Appl) u2 t3)
λu2:T.λ:T.pr0 u1 u2
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv3:T
.λt3:T
.eq
T
THead (Bind Abbr) v2 t2
THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2) t3)
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
case pr0_upsilon : b:B H1:not (eq B b Abst) v1:T v2:T H2:pr0 v1 v2 u0:T u2:T H4:pr0 u0 u2 t0:T t2:T H6:pr0 t0 t2 ⇒
the thesis becomes
∀H8:eq
T
THead (Flat Appl) v1 (THead (Bind b) u0 t0)
THead (Flat Appl) u1 t1
.or3
ex3_2
T
T
λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) u3 t3
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T
.λ:T
.λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind Abbr) u3 t3
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
(H3) by induction hypothesis we know
eq T v1 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu2:T.λt2:T.eq T v2 (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T v2 (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 z1 t2
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu2:T
.λv3:T.λt2:T.eq T v2 (THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2)
(H5) by induction hypothesis we know
eq T u0 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu3:T.λt2:T.eq T u2 (THead (Flat Appl) u3 t2) λu3:T.λ:T.pr0 u1 u3 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt2:T.eq T u2 (THead (Bind Abbr) u3 t2)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt2:T.pr0 z1 t2
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T.λt2:T.eq T u2 (THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t2))
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2)
(H7) by induction hypothesis we know
eq T t0 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu3:T.λt3:T.eq T t2 (THead (Flat Appl) u3 t3) λu3:T.λ:T.pr0 u1 u3 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T t2 (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T.λt3:T.eq T t2 (THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3))
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
suppose H8:
eq
T
THead (Flat Appl) v1 (THead (Bind b) u0 t0)
THead (Flat Appl) u1 t1
(H9)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u0 t0) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t ⇒t
<λ:T.T> CASE THead (Flat Appl) u1 t1 OF TSort ⇒v1 | TLRef ⇒v1 | THead t ⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t ⇒t
THead (Flat Appl) v1 (THead (Bind b) u0 t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t ⇒t
THead (Flat Appl) u1 t1
end of H9
(h1)
(H10)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u0 t0) OF
TSort ⇒THead (Bind b) u0 t0
| TLRef ⇒THead (Bind b) u0 t0
| THead t⇒t
<λ:T.T>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒THead (Bind b) u0 t0
| TLRef ⇒THead (Bind b) u0 t0
| THead t⇒t
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind b) u0 t0
| TLRef ⇒THead (Bind b) u0 t0
| THead t⇒t
THead (Flat Appl) v1 (THead (Bind b) u0 t0)
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind b) u0 t0
| TLRef ⇒THead (Bind b) u0 t0
| THead t⇒t
THead (Flat Appl) u1 t1
end of H10
suppose H11: eq T v1 u1
(H12)
we proceed by induction on H11 to prove
eq T u1 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu3:T.λt3:T.eq T v2 (THead (Flat Appl) u3 t3) λu3:T.λ:T.pr0 u1 u3 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T v2 (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T.λt3:T.eq T v2 (THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3))
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq T u1 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu3:T.λt3:T.eq T v2 (THead (Flat Appl) u3 t3) λu3:T.λ:T.pr0 u1 u3 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T v2 (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T.λt3:T.eq T v2 (THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3))
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
end of H12
(H13)
we proceed by induction on H11 to prove pr0 u1 v2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
pr0 u1 v2
end of H13
consider H10
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u0 t0) OF
TSort ⇒THead (Bind b) u0 t0
| TLRef ⇒THead (Bind b) u0 t0
| THead t⇒t
<λ:T.T>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒THead (Bind b) u0 t0
| TLRef ⇒THead (Bind b) u0 t0
| THead t⇒t
that is equivalent to eq T (THead (Bind b) u0 t0) t1
we proceed by induction on the previous result to prove
or3
ex3_2
T
T
λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) u3 t3
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T
.λ:T
.λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind Abbr) u3 t3
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
case refl_equal : ⇒
the thesis becomes
or3
ex3_2
T
T
λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) u3 t3
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 (THead (Bind b) u0 t0) t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T (THead (Bind b) u0 t0) (THead (Bind Abst) y1 z1)
λ:T
.λ:T
.λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind Abbr) u3 t3
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T (THead (Bind b) u0 t0) (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
(h1)
by (refl_equal . .)
eq T (THead (Bind b) u0 t0) (THead (Bind b) u0 t0)
end of h1
(h2)
by (refl_equal . .)
eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
end of h2
by (ex6_6_intro . . . . . . . . . . . . . . . . . . H1 h1 h2 H13 H4 H6)
we proved
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T (THead (Bind b) u0 t0) (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
by (or3_intro2 . . . previous)
or3
ex3_2
T
T
λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) u3 t3
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 (THead (Bind b) u0 t0) t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T (THead (Bind b) u0 t0) (THead (Bind Abst) y1 z1)
λ:T
.λ:T
.λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind Abbr) u3 t3
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T (THead (Bind b) u0 t0) (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
we proved
or3
ex3_2
T
T
λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) u3 t3
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T
.λ:T
.λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind Abbr) u3 t3
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
eq T v1 u1
→(or3
ex3_2
T
T
λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) u3 t3
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T
.λ:T
.λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind Abbr) u3 t3
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
end of h1
(h2)
consider H9
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u0 t0) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t ⇒t
<λ:T.T> CASE THead (Flat Appl) u1 t1 OF TSort ⇒v1 | TLRef ⇒v1 | THead t ⇒t
eq T v1 u1
end of h2
by (h1 h2)
we proved
or3
ex3_2
T
T
λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) u3 t3
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T
.λ:T
.λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind Abbr) u3 t3
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
∀H8:eq
T
THead (Flat Appl) v1 (THead (Bind b) u0 t0)
THead (Flat Appl) u1 t1
.or3
ex3_2
T
T
λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) u3 t3
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T
.λ:T
.λu3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind Abbr) u3 t3
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu3:T
.λv3:T
.λt3:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Bind b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv3:T.λ:T.pr0 y1 v3
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
case pr0_delta : u0:T u2:T :pr0 u0 u2 t0:T t2:T :pr0 t0 t2 w:T :subst0 O u2 t2 w ⇒
the thesis becomes
∀H6:eq T (THead (Bind Abbr) u0 t0) (THead (Flat Appl) u1 t1)
.or3
ex3_2
T
T
λu3:T.λt3:T.eq T (THead (Bind Abbr) u2 w) (THead (Flat Appl) u3 t3)
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T
.eq
T
THead (Bind Abbr) u2 w
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
() by induction hypothesis we know
eq T u0 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu3:T.λt2:T.eq T u2 (THead (Flat Appl) u3 t2) λu3:T.λ:T.pr0 u1 u3 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt2:T.eq T u2 (THead (Bind Abbr) u3 t2)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt2:T.eq T u2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t2))
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2)
() by induction hypothesis we know
eq T t0 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu3:T.λt3:T.eq T t2 (THead (Flat Appl) u3 t3) λu3:T.λ:T.pr0 u1 u3 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T t2 (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T.eq T t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3))
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
suppose H6: eq T (THead (Bind Abbr) u0 t0) (THead (Flat Appl) u1 t1)
(H7)
we proceed by induction on H6 to prove
<λ:T.Prop>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind Abbr) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind Abbr) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
end of H7
consider H7
we proved
<λ:T.Prop>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or3
ex3_2
T
T
λu3:T.λt3:T.eq T (THead (Bind Abbr) u2 w) (THead (Flat Appl) u3 t3)
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T
.eq
T
THead (Bind Abbr) u2 w
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
we proved
or3
ex3_2
T
T
λu3:T.λt3:T.eq T (THead (Bind Abbr) u2 w) (THead (Flat Appl) u3 t3)
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T
.eq
T
THead (Bind Abbr) u2 w
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
∀H6:eq T (THead (Bind Abbr) u0 t0) (THead (Flat Appl) u1 t1)
.or3
ex3_2
T
T
λu3:T.λt3:T.eq T (THead (Bind Abbr) u2 w) (THead (Flat Appl) u3 t3)
λu3:T.λ:T.pr0 u1 u3
λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu3:T.λt3:T.eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u3 t3)
λ:T.λ:T.λu3:T.λ:T.pr0 u1 u3
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu3:T
.λv2:T
.λt3:T
.eq
T
THead (Bind Abbr) u2 w
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)
λ:B.λ:T.λ:T.λu3:T.λ:T.λ:T.pr0 u1 u3
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
case pr0_zeta : b:B :not (eq B b Abst) t0:T t2:T :pr0 t0 t2 u:T ⇒
the thesis becomes
∀H4:eq T (THead (Bind b) u (lift (S O) O t0)) (THead (Flat Appl) u1 t1)
.or3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu2:T
.λv2:T.λt3:T.eq T t2 (THead (Bind b0) v2 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
() by induction hypothesis we know
eq T t0 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu2:T
.λv2:T.λt3:T.eq T t2 (THead (Bind b0) v2 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
suppose H4:
eq T (THead (Bind b) u (lift (S O) O t0)) (THead (Flat Appl) u1 t1)
(H5)
we proceed by induction on H4 to prove
<λ:T.Prop>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind b) u (lift (S O) O t0) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) u (lift (S O) O t0) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
end of H5
consider H5
we proved
<λ:T.Prop>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu2:T
.λv2:T.λt3:T.eq T t2 (THead (Bind b0) v2 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
we proved
or3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu2:T
.λv2:T.λt3:T.eq T t2 (THead (Bind b0) v2 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
∀H4:eq T (THead (Bind b) u (lift (S O) O t0)) (THead (Flat Appl) u1 t1)
.or3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
ex6_6
B
T
T
T
T
T
λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst)
λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T t1 (THead (Bind b0) y1 z1)
λb0:B
.λ:T
.λ:T
.λu2:T
.λv2:T.λt3:T.eq T t2 (THead (Bind b0) v2 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
case pr0_tau : t0:T t2:T :pr0 t0 t2 u:T ⇒
the thesis becomes
∀H3:eq T (THead (Flat Cast) u t0) (THead (Flat Appl) u1 t1)
.or3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt3:T.eq T t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
() by induction hypothesis we know
eq T t0 (THead (Flat Appl) u1 t1)
→(or3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt3:T.eq T t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3)
suppose H3: eq T (THead (Flat Cast) u t0) (THead (Flat Appl) u1 t1)
(H4)
we proceed by induction on H3 to prove
<λ:T.Prop>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Cast) u t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Cast) u t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
<λ:T.Prop>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
end of H4
consider H4
we proved
<λ:T.Prop>
CASE THead (Flat Appl) u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
or3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt3:T.eq T t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
we proved
or3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt3:T.eq T t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
∀H3:eq T (THead (Flat Cast) u t0) (THead (Flat Appl) u1 t1)
.or3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3
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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt3:T.eq T t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t3))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3
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.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt2:T
.eq T x (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2)
we proved
∀y:T
.pr0 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.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt2:T
.eq T x (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2))
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.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt2:T
.eq T x (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2
we proved
∀u1:T
.∀t1:T
.∀x:T
.pr0 (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.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t1 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt2:T
.eq T x (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2)