DEFINITION pr0_gen_lift()
TYPE =
∀t1:T.∀x:T.∀h:nat.∀d:nat.(pr0 (lift h d t1) x)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr0 t1 t2)
BODY =
assume t1: T
assume x: T
assume h: nat
assume d: nat
suppose H: pr0 (lift h d t1) x
assume y: T
suppose H0: pr0 y x
we proceed by induction on H0 to prove ∀x0:T.∀x1:nat.(eq T y (lift h x1 x0))→(ex2 T λt2:T.eq T x (lift h x1 t2) λt2:T.pr0 x0 t2)
case pr0_refl : t:T ⇒
the thesis becomes ∀x0:T.∀x1:nat.∀H1:(eq T t (lift h x1 x0)).(ex2 T λt2:T.eq T t (lift h x1 t2) λt2:T.pr0 x0 t2)
assume x0: T
assume x1: nat
suppose H1: eq T t (lift h x1 x0)
by (pr0_refl .)
we proved pr0 x0 x0
by (ex_intro2 . . . . H1 previous)
we proved ex2 T λt2:T.eq T t (lift h x1 t2) λt2:T.pr0 x0 t2
∀x0:T.∀x1:nat.∀H1:(eq T t (lift h x1 x0)).(ex2 T λt2:T.eq T t (lift h x1 t2) λt2:T.pr0 x0 t2)
case pr0_comp : u1:T u2:T :pr0 u1 u2 t2:T t3:T :pr0 t2 t3 k:K ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H5:(eq T (THead k u1 t2) (lift h x1 x0)).(ex2 T λt4:T.eq T (THead k u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4)
(H2) by induction hypothesis we know ∀x0:T.∀x1:nat.(eq T u1 (lift h x1 x0))→(ex2 T λt2:T.eq T u2 (lift h x1 t2) λt2:T.pr0 x0 t2)
(H4) by induction hypothesis we know ∀x0:T.∀x1:nat.(eq T t2 (lift h x1 x0))→(ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4)
assume x0: T
assume x1: nat
suppose H5: eq T (THead k u1 t2) (lift h x1 x0)
assume b: B
suppose H6: eq T (THead (Bind b) u1 t2) (lift h x1 x0)
by (lift_gen_bind . . . . . . H6)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Bind b) y z)
λy:T.λ:T.eq T u1 (lift h x1 y)
λ:T.λz:T.eq T t2 (lift h (S x1) z)
we proceed by induction on the previous result to prove ex2 T λt4:T.eq T (THead (Bind b) u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
case ex3_2_intro : x2:T x3:T H7:eq T x0 (THead (Bind b) x2 x3) H8:eq T u1 (lift h x1 x2) H9:eq T t2 (lift h (S x1) x3) ⇒
the thesis becomes ex2 T λt4:T.eq T (THead (Bind b) u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
by (H4 . . H9)
we proved ex2 T λt4:T.eq T t3 (lift h (S x1) t4) λt4:T.pr0 x3 t4
we proceed by induction on the previous result to prove
ex2 T λt4:T.eq T (THead (Bind b) u2 t3) (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 x3) t4
case ex_intro2 : x4:T H_x:eq T t3 (lift h (S x1) x4) H10:pr0 x3 x4 ⇒
the thesis becomes
ex2 T λt4:T.eq T (THead (Bind b) u2 t3) (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 x3) t4
by (H2 . . H8)
we proved ex2 T λt2:T.eq T u2 (lift h x1 t2) λt2:T.pr0 x2 t2
we proceed by induction on the previous result to prove
ex2
T
λt4:T.eq T (THead (Bind b) u2 (lift h (S x1) x4)) (lift h x1 t4)
λt4:T.pr0 (THead (Bind b) x2 x3) t4
case ex_intro2 : x5:T H_x0:eq T u2 (lift h x1 x5) H11:pr0 x2 x5 ⇒
the thesis becomes
ex2
T
λt4:T.eq T (THead (Bind b) u2 (lift h (S x1) x4)) (lift h x1 t4)
λt4:T.pr0 (THead (Bind b) x2 x3) t4
(h1)
by (lift_bind . . . . .)
we proved
eq
T
lift h x1 (THead (Bind b) x5 x4)
THead (Bind b) (lift h x1 x5) (lift h (S x1) x4)
by (sym_eq . . . previous)
eq
T
THead (Bind b) (lift h x1 x5) (lift h (S x1) x4)
lift h x1 (THead (Bind b) x5 x4)
end of h1
(h2)
by (pr0_comp . . H11 . . H10 .)
pr0 (THead (Bind b) x2 x3) (THead (Bind b) x5 x4)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt4:T.eq T (THead (Bind b) (lift h x1 x5) (lift h (S x1) x4)) (lift h x1 t4)
λt4:T.pr0 (THead (Bind b) x2 x3) t4
by (eq_ind_r . . . previous . H_x0)
ex2
T
λt4:T.eq T (THead (Bind b) u2 (lift h (S x1) x4)) (lift h x1 t4)
λt4:T.pr0 (THead (Bind b) x2 x3) t4
we proved
ex2
T
λt4:T.eq T (THead (Bind b) u2 (lift h (S x1) x4)) (lift h x1 t4)
λt4:T.pr0 (THead (Bind b) x2 x3) t4
by (eq_ind_r . . . previous . H_x)
ex2 T λt4:T.eq T (THead (Bind b) u2 t3) (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 x3) t4
we proved
ex2 T λt4:T.eq T (THead (Bind b) u2 t3) (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 x3) t4
by (eq_ind_r . . . previous . H7)
ex2 T λt4:T.eq T (THead (Bind b) u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
we proved ex2 T λt4:T.eq T (THead (Bind b) u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
∀H6:eq T (THead (Bind b) u1 t2) (lift h x1 x0)
.ex2 T λt4:T.eq T (THead (Bind b) u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
assume f: F
suppose H6: eq T (THead (Flat f) u1 t2) (lift h x1 x0)
by (lift_gen_flat . . . . . . H6)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Flat f) y z)
λy:T.λ:T.eq T u1 (lift h x1 y)
λ:T.λz:T.eq T t2 (lift h x1 z)
we proceed by induction on the previous result to prove ex2 T λt4:T.eq T (THead (Flat f) u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
case ex3_2_intro : x2:T x3:T H7:eq T x0 (THead (Flat f) x2 x3) H8:eq T u1 (lift h x1 x2) H9:eq T t2 (lift h x1 x3) ⇒
the thesis becomes ex2 T λt4:T.eq T (THead (Flat f) u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
by (H4 . . H9)
we proved ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x3 t4
we proceed by induction on the previous result to prove
ex2 T λt4:T.eq T (THead (Flat f) u2 t3) (lift h x1 t4) λt4:T.pr0 (THead (Flat f) x2 x3) t4
case ex_intro2 : x4:T H_x:eq T t3 (lift h x1 x4) H10:pr0 x3 x4 ⇒
the thesis becomes
ex2 T λt4:T.eq T (THead (Flat f) u2 t3) (lift h x1 t4) λt4:T.pr0 (THead (Flat f) x2 x3) t4
by (H2 . . H8)
we proved ex2 T λt2:T.eq T u2 (lift h x1 t2) λt2:T.pr0 x2 t2
we proceed by induction on the previous result to prove
ex2
T
λt4:T.eq T (THead (Flat f) u2 (lift h x1 x4)) (lift h x1 t4)
λt4:T.pr0 (THead (Flat f) x2 x3) t4
case ex_intro2 : x5:T H_x0:eq T u2 (lift h x1 x5) H11:pr0 x2 x5 ⇒
the thesis becomes
ex2
T
λt4:T.eq T (THead (Flat f) u2 (lift h x1 x4)) (lift h x1 t4)
λt4:T.pr0 (THead (Flat f) x2 x3) t4
(h1)
by (lift_flat . . . . .)
we proved
eq
T
lift h x1 (THead (Flat f) x5 x4)
THead (Flat f) (lift h x1 x5) (lift h x1 x4)
by (sym_eq . . . previous)
eq
T
THead (Flat f) (lift h x1 x5) (lift h x1 x4)
lift h x1 (THead (Flat f) x5 x4)
end of h1
(h2)
by (pr0_comp . . H11 . . H10 .)
pr0 (THead (Flat f) x2 x3) (THead (Flat f) x5 x4)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt4:T.eq T (THead (Flat f) (lift h x1 x5) (lift h x1 x4)) (lift h x1 t4)
λt4:T.pr0 (THead (Flat f) x2 x3) t4
by (eq_ind_r . . . previous . H_x0)
ex2
T
λt4:T.eq T (THead (Flat f) u2 (lift h x1 x4)) (lift h x1 t4)
λt4:T.pr0 (THead (Flat f) x2 x3) t4
we proved
ex2
T
λt4:T.eq T (THead (Flat f) u2 (lift h x1 x4)) (lift h x1 t4)
λt4:T.pr0 (THead (Flat f) x2 x3) t4
by (eq_ind_r . . . previous . H_x)
ex2 T λt4:T.eq T (THead (Flat f) u2 t3) (lift h x1 t4) λt4:T.pr0 (THead (Flat f) x2 x3) t4
we proved
ex2 T λt4:T.eq T (THead (Flat f) u2 t3) (lift h x1 t4) λt4:T.pr0 (THead (Flat f) x2 x3) t4
by (eq_ind_r . . . previous . H7)
ex2 T λt4:T.eq T (THead (Flat f) u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
we proved ex2 T λt4:T.eq T (THead (Flat f) u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
∀H6:eq T (THead (Flat f) u1 t2) (lift h x1 x0)
.ex2 T λt4:T.eq T (THead (Flat f) u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
by (previous . H5)
we proved ex2 T λt4:T.eq T (THead k u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
∀x0:T
.∀x1:nat
.∀H5:(eq T (THead k u1 t2) (lift h x1 x0)).(ex2 T λt4:T.eq T (THead k u2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4)
case pr0_beta : u:T v1:T v2:T :pr0 v1 v2 t2:T t3:T :pr0 t2 t3 ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H5:eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t2)) (lift h x1 x0)
.ex2 T λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
(H2) by induction hypothesis we know ∀x0:T.∀x1:nat.(eq T v1 (lift h x1 x0))→(ex2 T λt2:T.eq T v2 (lift h x1 t2) λt2:T.pr0 x0 t2)
(H4) by induction hypothesis we know ∀x0:T.∀x1:nat.(eq T t2 (lift h x1 x0))→(ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4)
assume x0: T
assume x1: nat
suppose H5: eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t2)) (lift h x1 x0)
by (lift_gen_flat . . . . . . H5)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Flat Appl) y z)
λy:T.λ:T.eq T v1 (lift h x1 y)
λ:T.λz:T.eq T (THead (Bind Abst) u t2) (lift h x1 z)
we proceed by induction on the previous result to prove ex2 T λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
case ex3_2_intro : x2:T x3:T H6:eq T x0 (THead (Flat Appl) x2 x3) H7:eq T v1 (lift h x1 x2) H8:eq T (THead (Bind Abst) u t2) (lift h x1 x3) ⇒
the thesis becomes ex2 T λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
by (lift_gen_bind . . . . . . H8)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x3 (THead (Bind Abst) y z)
λy:T.λ:T.eq T u (lift h x1 y)
λ:T.λz:T.eq T t2 (lift h (S x1) z)
we proceed by induction on the previous result to prove
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 x3) t4
case ex3_2_intro : x4:T x5:T H9:eq T x3 (THead (Bind Abst) x4 x5) :eq T u (lift h x1 x4) H11:eq T t2 (lift h (S x1) x5) ⇒
the thesis becomes
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 x3) t4
by (H4 . . H11)
we proved ex2 T λt4:T.eq T t3 (lift h (S x1) t4) λt4:T.pr0 x5 t4
we proceed by induction on the previous result to prove
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4
case ex_intro2 : x6:T H_x:eq T t3 (lift h (S x1) x6) H12:pr0 x5 x6 ⇒
the thesis becomes
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4
by (H2 . . H7)
we proved ex2 T λt2:T.eq T v2 (lift h x1 t2) λt2:T.pr0 x2 t2
we proceed by induction on the previous result to prove
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 (lift h (S x1) x6)) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4
case ex_intro2 : x7:T H_x0:eq T v2 (lift h x1 x7) H13:pr0 x2 x7 ⇒
the thesis becomes
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 (lift h (S x1) x6)) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4
(h1)
by (lift_bind . . . . .)
we proved
eq
T
lift h x1 (THead (Bind Abbr) x7 x6)
THead (Bind Abbr) (lift h x1 x7) (lift h (S x1) x6)
by (sym_eq . . . previous)
eq
T
THead (Bind Abbr) (lift h x1 x7) (lift h (S x1) x6)
lift h x1 (THead (Bind Abbr) x7 x6)
end of h1
(h2)
by (pr0_beta . . . H13 . . H12)
pr0
THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)
THead (Bind Abbr) x7 x6
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt4:T.eq T (THead (Bind Abbr) (lift h x1 x7) (lift h (S x1) x6)) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4
by (eq_ind_r . . . previous . H_x0)
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 (lift h (S x1) x6)) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4
we proved
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 (lift h (S x1) x6)) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4
by (eq_ind_r . . . previous . H_x)
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4
we proved
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4
by (eq_ind_r . . . previous . H9)
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 x3) t4
we proved
ex2
T
λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4)
λt4:T.pr0 (THead (Flat Appl) x2 x3) t4
by (eq_ind_r . . . previous . H6)
ex2 T λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
we proved ex2 T λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
∀x0:T
.∀x1:nat
.∀H5:eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t2)) (lift h x1 x0)
.ex2 T λt4:T.eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4) λt4:T.pr0 x0 t4
case pr0_upsilon : b:B H1:not (eq B b Abst) v1:T v2:T :pr0 v1 v2 u1:T u2:T :pr0 u1 u2 t2:T t3:T :pr0 t2 t3 ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H8:eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t2)) (lift h x1 x0)
.ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 x0 t4
(H3) by induction hypothesis we know ∀x0:T.∀x1:nat.(eq T v1 (lift h x1 x0))→(ex2 T λt2:T.eq T v2 (lift h x1 t2) λt2:T.pr0 x0 t2)
(H5) by induction hypothesis we know ∀x0:T.∀x1:nat.(eq T u1 (lift h x1 x0))→(ex2 T λt2:T.eq T u2 (lift h x1 t2) λt2:T.pr0 x0 t2)
(H7) by induction hypothesis we know ∀x0:T.∀x1:nat.(eq T t2 (lift h x1 x0))→(ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4)
assume x0: T
assume x1: nat
suppose H8: eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t2)) (lift h x1 x0)
by (lift_gen_flat . . . . . . H8)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Flat Appl) y z)
λy:T.λ:T.eq T v1 (lift h x1 y)
λ:T.λz:T.eq T (THead (Bind b) u1 t2) (lift h x1 z)
we proceed by induction on the previous result to prove
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 x0 t4
case ex3_2_intro : x2:T x3:T H9:eq T x0 (THead (Flat Appl) x2 x3) H10:eq T v1 (lift h x1 x2) H11:eq T (THead (Bind b) u1 t2) (lift h x1 x3) ⇒
the thesis becomes
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 x0 t4
by (lift_gen_bind . . . . . . H11)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x3 (THead (Bind b) y z)
λy:T.λ:T.eq T u1 (lift h x1 y)
λ:T.λz:T.eq T t2 (lift h (S x1) z)
we proceed by induction on the previous result to prove
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 x3) t4
case ex3_2_intro : x4:T x5:T H12:eq T x3 (THead (Bind b) x4 x5) H13:eq T u1 (lift h x1 x4) H14:eq T t2 (lift h (S x1) x5) ⇒
the thesis becomes
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 x3) t4
by (H7 . . H14)
we proved ex2 T λt4:T.eq T t3 (lift h (S x1) t4) λt4:T.pr0 x5 t4
we proceed by induction on the previous result to prove
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
case ex_intro2 : x6:T H_x:eq T t3 (lift h (S x1) x6) H15:pr0 x5 x6 ⇒
the thesis becomes
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
by (H5 . . H13)
we proved ex2 T λt2:T.eq T u2 (lift h x1 t2) λt2:T.pr0 x4 t2
we proceed by induction on the previous result to prove
ex2
T
λt4:T
.eq
T
THead
Bind b
u2
THead (Flat Appl) (lift (S O) O v2) (lift h (S x1) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
case ex_intro2 : x7:T H_x0:eq T u2 (lift h x1 x7) H16:pr0 x4 x7 ⇒
the thesis becomes
ex2
T
λt4:T
.eq
T
THead
Bind b
u2
THead (Flat Appl) (lift (S O) O v2) (lift h (S x1) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
by (H3 . . H10)
we proved ex2 T λt2:T.eq T v2 (lift h x1 t2) λt2:T.pr0 x2 t2
we proceed by induction on the previous result to prove
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
THead (Flat Appl) (lift (S O) O v2) (lift h (S x1) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
case ex_intro2 : x8:T H_x1:eq T v2 (lift h x1 x8) H17:pr0 x2 x8 ⇒
the thesis becomes
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
THead (Flat Appl) (lift (S O) O v2) (lift h (S x1) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
by (le_O_n .)
we proved le O x1
by (lift_d . . . . . previous)
we proved
eq
T
lift h (plus (S O) x1) (lift (S O) O x8)
lift (S O) O (lift h x1 x8)
we proceed by induction on the previous result to prove
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
THead (Flat Appl) (lift (S O) O (lift h x1 x8)) (lift h (S x1) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
case refl_equal : ⇒
the thesis becomes
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
THead
Flat Appl
lift h (plus (S O) x1) (lift (S O) O x8)
lift h (S x1) x6
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
by (lift_flat . . . . .)
we proved
eq
T
lift h (S x1) (THead (Flat Appl) (lift (S O) O x8) x6)
THead
Flat Appl
lift h (S x1) (lift (S O) O x8)
lift h (S x1) x6
we proceed by induction on the previous result to prove
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
THead
Flat Appl
lift h (S x1) (lift (S O) O x8)
lift h (S x1) x6
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
case refl_equal : ⇒
the thesis becomes
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
lift h (S x1) (THead (Flat Appl) (lift (S O) O x8) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
(h1)
by (lift_bind . . . . .)
we proved
eq
T
lift
h
x1
THead (Bind b) x7 (THead (Flat Appl) (lift (S O) O x8) x6)
THead
Bind b
lift h x1 x7
lift h (S x1) (THead (Flat Appl) (lift (S O) O x8) x6)
by (sym_eq . . . previous)
eq
T
THead
Bind b
lift h x1 x7
lift h (S x1) (THead (Flat Appl) (lift (S O) O x8) x6)
lift
h
x1
THead (Bind b) x7 (THead (Flat Appl) (lift (S O) O x8) x6)
end of h1
(h2)
by (pr0_upsilon . H1 . . H17 . . H16 . . H15)
pr0
THead (Flat Appl) x2 (THead (Bind b) x4 x5)
THead (Bind b) x7 (THead (Flat Appl) (lift (S O) O x8) x6)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
lift h (S x1) (THead (Flat Appl) (lift (S O) O x8) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
we proved
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
THead
Flat Appl
lift h (S x1) (lift (S O) O x8)
lift h (S x1) x6
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
THead
Flat Appl
lift h (plus (S O) x1) (lift (S O) O x8)
lift h (S x1) x6
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
we proved
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
THead (Flat Appl) (lift (S O) O (lift h x1 x8)) (lift h (S x1) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
by (eq_ind_r . . . previous . H_x1)
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
THead (Flat Appl) (lift (S O) O v2) (lift h (S x1) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
we proved
ex2
T
λt4:T
.eq
T
THead
Bind b
lift h x1 x7
THead (Flat Appl) (lift (S O) O v2) (lift h (S x1) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
by (eq_ind_r . . . previous . H_x0)
ex2
T
λt4:T
.eq
T
THead
Bind b
u2
THead (Flat Appl) (lift (S O) O v2) (lift h (S x1) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
we proved
ex2
T
λt4:T
.eq
T
THead
Bind b
u2
THead (Flat Appl) (lift (S O) O v2) (lift h (S x1) x6)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
by (eq_ind_r . . . previous . H_x)
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
we proved
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4
by (eq_ind_r . . . previous . H12)
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 x3) t4
we proved
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 (THead (Flat Appl) x2 x3) t4
by (eq_ind_r . . . previous . H9)
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 x0 t4
we proved
ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 x0 t4
∀x0:T
.∀x1:nat
.∀H8:eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t2)) (lift h x1 x0)
.ex2
T
λt4:T
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)
lift h x1 t4
λt4:T.pr0 x0 t4
case pr0_delta : u1:T u2:T :pr0 u1 u2 t2:T t3:T :pr0 t2 t3 w:T H5:subst0 O u2 t3 w ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H6:eq T (THead (Bind Abbr) u1 t2) (lift h x1 x0)
.ex2 T λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4) λt4:T.pr0 x0 t4
(H2) by induction hypothesis we know ∀x0:T.∀x1:nat.(eq T u1 (lift h x1 x0))→(ex2 T λt2:T.eq T u2 (lift h x1 t2) λt2:T.pr0 x0 t2)
(H4) by induction hypothesis we know ∀x0:T.∀x1:nat.(eq T t2 (lift h x1 x0))→(ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4)
assume x0: T
assume x1: nat
suppose H6: eq T (THead (Bind Abbr) u1 t2) (lift h x1 x0)
by (lift_gen_bind . . . . . . H6)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Bind Abbr) y z)
λy:T.λ:T.eq T u1 (lift h x1 y)
λ:T.λz:T.eq T t2 (lift h (S x1) z)
we proceed by induction on the previous result to prove ex2 T λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4) λt4:T.pr0 x0 t4
case ex3_2_intro : x2:T x3:T H7:eq T x0 (THead (Bind Abbr) x2 x3) H8:eq T u1 (lift h x1 x2) H9:eq T t2 (lift h (S x1) x3) ⇒
the thesis becomes ex2 T λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4) λt4:T.pr0 x0 t4
by (H4 . . H9)
we proved ex2 T λt4:T.eq T t3 (lift h (S x1) t4) λt4:T.pr0 x3 t4
we proceed by induction on the previous result to prove
ex2
T
λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4)
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
case ex_intro2 : x4:T H_x:eq T t3 (lift h (S x1) x4) H10:pr0 x3 x4 ⇒
the thesis becomes
ex2
T
λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4)
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
(H11)
we proceed by induction on H_x to prove subst0 O u2 (lift h (S x1) x4) w
case refl_equal : ⇒
the thesis becomes the hypothesis H5
subst0 O u2 (lift h (S x1) x4) w
end of H11
by (H2 . . H8)
we proved ex2 T λt2:T.eq T u2 (lift h x1 t2) λt2:T.pr0 x2 t2
we proceed by induction on the previous result to prove
ex2
T
λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4)
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
case ex_intro2 : x5:T H_x0:eq T u2 (lift h x1 x5) H12:pr0 x2 x5 ⇒
the thesis becomes
ex2
T
λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4)
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
(H13)
we proceed by induction on H_x0 to prove subst0 O (lift h x1 x5) (lift h (S x1) x4) w
case refl_equal : ⇒
the thesis becomes the hypothesis H11
subst0 O (lift h x1 x5) (lift h (S x1) x4) w
end of H13
(H14)
by (refl_equal . .)
eq nat (S (plus O x1)) (S (plus O x1))
end of H14
(H15)
consider H14
we proved eq nat (S (plus O x1)) (S (plus O x1))
that is equivalent to eq nat (S x1) (S (plus O x1))
we proceed by induction on the previous result to prove subst0 O (lift h x1 x5) (lift h (S (plus O x1)) x4) w
case refl_equal : ⇒
the thesis becomes the hypothesis H13
subst0 O (lift h x1 x5) (lift h (S (plus O x1)) x4) w
end of H15
by (subst0_gen_lift_lt . . . . . . H15)
we proved ex2 T λt2:T.eq T w (lift h (S (plus O x1)) t2) λt2:T.subst0 O x5 x4 t2
we proceed by induction on the previous result to prove
ex2
T
λt4:T.eq T (THead (Bind Abbr) (lift h x1 x5) w) (lift h x1 t4)
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
case ex_intro2 : x6:T H16:eq T w (lift h (S (plus O x1)) x6) H17:subst0 O x5 x4 x6 ⇒
the thesis becomes
ex2
T
λt4:T.eq T (THead (Bind Abbr) (lift h x1 x5) w) (lift h x1 t4)
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
(h1)
by (lift_bind . . . . .)
we proved
eq
T
lift h (plus O x1) (THead (Bind Abbr) x5 x6)
THead (Bind Abbr) (lift h (plus O x1) x5) (lift h (S (plus O x1)) x6)
that is equivalent to
eq
T
lift h x1 (THead (Bind Abbr) x5 x6)
THead (Bind Abbr) (lift h x1 x5) (lift h (S (plus O x1)) x6)
by (sym_eq . . . previous)
eq
T
THead (Bind Abbr) (lift h x1 x5) (lift h (S (plus O x1)) x6)
lift h x1 (THead (Bind Abbr) x5 x6)
end of h1
(h2)
by (pr0_delta . . H12 . . H10 . H17)
pr0 (THead (Bind Abbr) x2 x3) (THead (Bind Abbr) x5 x6)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt4:T
.eq
T
THead (Bind Abbr) (lift h x1 x5) (lift h (S (plus O x1)) x6)
lift h x1 t4
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
by (eq_ind_r . . . previous . H16)
ex2
T
λt4:T.eq T (THead (Bind Abbr) (lift h x1 x5) w) (lift h x1 t4)
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
we proved
ex2
T
λt4:T.eq T (THead (Bind Abbr) (lift h x1 x5) w) (lift h x1 t4)
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
by (eq_ind_r . . . previous . H_x0)
ex2
T
λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4)
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
ex2
T
λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4)
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
we proved
ex2
T
λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4)
λt4:T.pr0 (THead (Bind Abbr) x2 x3) t4
by (eq_ind_r . . . previous . H7)
ex2 T λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4) λt4:T.pr0 x0 t4
we proved ex2 T λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4) λt4:T.pr0 x0 t4
∀x0:T
.∀x1:nat
.∀H6:eq T (THead (Bind Abbr) u1 t2) (lift h x1 x0)
.ex2 T λt4:T.eq T (THead (Bind Abbr) u2 w) (lift h x1 t4) λt4:T.pr0 x0 t4
case pr0_zeta : b:B H1:not (eq B b Abst) t2:T t3:T :pr0 t2 t3 u:T ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H4:eq T (THead (Bind b) u (lift (S O) O t2)) (lift h x1 x0)
.ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
(H3) by induction hypothesis we know ∀x0:T.∀x1:nat.(eq T t2 (lift h x1 x0))→(ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4)
assume x0: T
assume x1: nat
suppose H4: eq T (THead (Bind b) u (lift (S O) O t2)) (lift h x1 x0)
by (lift_gen_bind . . . . . . H4)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Bind b) y z)
λy:T.λ:T.eq T u (lift h x1 y)
λ:T.λz:T.eq T (lift (S O) O t2) (lift h (S x1) z)
we proceed by induction on the previous result to prove ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
case ex3_2_intro : x2:T x3:T H5:eq T x0 (THead (Bind b) x2 x3) :eq T u (lift h x1 x2) H7:eq T (lift (S O) O t2) (lift h (S x1) x3) ⇒
the thesis becomes ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
(H8)
(h1)
by (refl_equal . .)
we proved eq nat (plus (S O) x1) (plus (S O) x1)
eq nat (S x1) (plus (S O) x1)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus x1 (S O)) (plus (S O) x1)
end of h2
by (eq_ind_r . . . h1 . h2)
eq nat (S x1) (plus x1 (S O))
end of H8
(H9)
we proceed by induction on H8 to prove eq T (lift (S O) O t2) (lift h (plus x1 (S O)) x3)
case refl_equal : ⇒
the thesis becomes the hypothesis H7
eq T (lift (S O) O t2) (lift h (plus x1 (S O)) x3)
end of H9
by (le_O_n .)
we proved le O x1
by (lift_gen_lift . . . . . . previous H9)
we proved ex2 T λt2:T.eq T x3 (lift (S O) O t2) λt2:T.eq T t2 (lift h x1 t2)
we proceed by induction on the previous result to prove ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 x3) t4
case ex_intro2 : x4:T H10:eq T x3 (lift (S O) O x4) H11:eq T t2 (lift h x1 x4) ⇒
the thesis becomes ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 x3) t4
by (H3 . . H11)
we proved ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x4 t4
we proceed by induction on the previous result to prove ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 (lift (S O) O x4)) t4
case ex_intro2 : x5:T H_x:eq T t3 (lift h x1 x5) H12:pr0 x4 x5 ⇒
the thesis becomes ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 (lift (S O) O x4)) t4
(h1)
by (refl_equal . .)
eq T (lift h x1 x5) (lift h x1 x5)
end of h1
(h2)
by (pr0_zeta . H1 . . H12 .)
pr0 (THead (Bind b) x2 (lift (S O) O x4)) x5
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt4:T.eq T (lift h x1 x5) (lift h x1 t4)
λt4:T.pr0 (THead (Bind b) x2 (lift (S O) O x4)) t4
by (eq_ind_r . . . previous . H_x)
ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 (lift (S O) O x4)) t4
we proved ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 (lift (S O) O x4)) t4
by (eq_ind_r . . . previous . H10)
ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 x3) t4
we proved ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Bind b) x2 x3) t4
by (eq_ind_r . . . previous . H5)
ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
we proved ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
∀x0:T
.∀x1:nat
.∀H4:eq T (THead (Bind b) u (lift (S O) O t2)) (lift h x1 x0)
.ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
case pr0_tau : t2:T t3:T :pr0 t2 t3 u:T ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H3:eq T (THead (Flat Cast) u t2) (lift h x1 x0)
.ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
(H2) by induction hypothesis we know ∀x0:T.∀x1:nat.(eq T t2 (lift h x1 x0))→(ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4)
assume x0: T
assume x1: nat
suppose H3: eq T (THead (Flat Cast) u t2) (lift h x1 x0)
by (lift_gen_flat . . . . . . H3)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Flat Cast) y z)
λy:T.λ:T.eq T u (lift h x1 y)
λ:T.λz:T.eq T t2 (lift h x1 z)
we proceed by induction on the previous result to prove ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
case ex3_2_intro : x2:T x3:T H4:eq T x0 (THead (Flat Cast) x2 x3) :eq T u (lift h x1 x2) H6:eq T t2 (lift h x1 x3) ⇒
the thesis becomes ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
by (H2 . . H6)
we proved ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x3 t4
we proceed by induction on the previous result to prove ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Flat Cast) x2 x3) t4
case ex_intro2 : x4:T H_x:eq T t3 (lift h x1 x4) H7:pr0 x3 x4 ⇒
the thesis becomes ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Flat Cast) x2 x3) t4
(h1)
by (refl_equal . .)
eq T (lift h x1 x4) (lift h x1 x4)
end of h1
(h2)
by (pr0_tau . . H7 .)
pr0 (THead (Flat Cast) x2 x3) x4
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 T λt4:T.eq T (lift h x1 x4) (lift h x1 t4) λt4:T.pr0 (THead (Flat Cast) x2 x3) t4
by (eq_ind_r . . . previous . H_x)
ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Flat Cast) x2 x3) t4
we proved ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 (THead (Flat Cast) x2 x3) t4
by (eq_ind_r . . . previous . H4)
ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
we proved ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
∀x0:T
.∀x1:nat
.∀H3:eq T (THead (Flat Cast) u t2) (lift h x1 x0)
.ex2 T λt4:T.eq T t3 (lift h x1 t4) λt4:T.pr0 x0 t4
we proved ∀x0:T.∀x1:nat.(eq T y (lift h x1 x0))→(ex2 T λt2:T.eq T x (lift h x1 t2) λt2:T.pr0 x0 t2)
by (unintro . . . previous)
we proved ∀x0:nat.(eq T y (lift h x0 t1))→(ex2 T λt2:T.eq T x (lift h x0 t2) λt2:T.pr0 t1 t2)
by (unintro . . . previous)
we proved (eq T y (lift h d t1))→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr0 t1 t2)
we proved
∀y:T
.pr0 y x
→(eq T y (lift h d t1))→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr0 t1 t2)
by (insert_eq . . . . previous H)
we proved ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr0 t1 t2
we proved ∀t1:T.∀x:T.∀h:nat.∀d:nat.(pr0 (lift h d t1) x)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr0 t1 t2)