DEFINITION pr0_lift()
TYPE =
∀t1:T.∀t2:T.(pr0 t1 t2)→∀h:nat.∀d:nat.(pr0 (lift h d t1) (lift h d t2))
BODY =
assume t1: T
assume t2: T
suppose H: pr0 t1 t2
we proceed by induction on H to prove ∀h:nat.∀d:nat.(pr0 (lift h d t1) (lift h d t2))
case pr0_refl : t:T ⇒
the thesis becomes ∀h:nat.∀d:nat.(pr0 (lift h d t) (lift h d t))
assume h: nat
assume d: nat
by (pr0_refl .)
we proved pr0 (lift h d t) (lift h d t)
∀h:nat.∀d:nat.(pr0 (lift h d t) (lift h d t))
case pr0_comp : u1:T u2:T :pr0 u1 u2 t3:T t4:T :pr0 t3 t4 k:K ⇒
the thesis becomes ∀h:nat.∀d:nat.(pr0 (lift h d (THead k u1 t3)) (lift h d (THead k u2 t4)))
(H1) by induction hypothesis we know ∀h:nat.∀d:nat.(pr0 (lift h d u1) (lift h d u2))
(H3) by induction hypothesis we know ∀h:nat.∀d:nat.(pr0 (lift h d t3) (lift h d t4))
assume h: nat
assume d: nat
(h1)
(h1)
(h1)
by (H1 . .)
pr0 (lift h d u1) (lift h d u2)
end of h1
(h2)
by (H3 . .)
pr0 (lift h (s k d) t3) (lift h (s k d) t4)
end of h2
by (pr0_comp . . h1 . . h2 .)
pr0
THead k (lift h d u1) (lift h (s k d) t3)
THead k (lift h d u2) (lift h (s k d) t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead k u2 t4)
THead k (lift h d u2) (lift h (s k d) t4)
end of h2
by (eq_ind_r . . . h1 . h2)
pr0 (THead k (lift h d u1) (lift h (s k d) t3)) (lift h d (THead k u2 t4))
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead k u1 t3)
THead k (lift h d u1) (lift h (s k d) t3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved pr0 (lift h d (THead k u1 t3)) (lift h d (THead k u2 t4))
∀h:nat.∀d:nat.(pr0 (lift h d (THead k u1 t3)) (lift h d (THead k u2 t4)))
case pr0_beta : u:T v1:T v2:T :pr0 v1 v2 t3:T t4:T :pr0 t3 t4 ⇒
the thesis becomes
∀h:nat
.∀d:nat
.pr0
lift h d (THead (Flat Appl) v1 (THead (Bind Abst) u t3))
lift h d (THead (Bind Abbr) v2 t4)
(H1) by induction hypothesis we know ∀h:nat.∀d:nat.(pr0 (lift h d v1) (lift h d v2))
(H3) by induction hypothesis we know ∀h:nat.∀d:nat.(pr0 (lift h d t3) (lift h d t4))
assume h: nat
assume d: nat
(h1)
(h1)
(h1)
(h1)
by (H1 . .)
pr0 (lift h d v1) (lift h d v2)
end of h1
(h2)
by (H3 . .)
we proved pr0 (lift h (s (Bind Abbr) d) t3) (lift h (s (Bind Abbr) d) t4)
pr0
lift h (s (Bind Abst) (s (Flat Appl) d)) t3
lift h (s (Bind Abbr) d) t4
end of h2
by (pr0_beta . . . h1 . . h2)
pr0
THead
Flat Appl
lift h d v1
THead
Bind Abst
lift h (s (Flat Appl) d) u
lift h (s (Bind Abst) (s (Flat Appl) d)) t3
THead (Bind Abbr) (lift h d v2) (lift h (s (Bind Abbr) d) t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Bind Abbr) v2 t4)
THead (Bind Abbr) (lift h d v2) (lift h (s (Bind Abbr) d) t4)
end of h2
by (eq_ind_r . . . h1 . h2)
pr0
THead
Flat Appl
lift h d v1
THead
Bind Abst
lift h (s (Flat Appl) d) u
lift h (s (Bind Abst) (s (Flat Appl) d)) t3
lift h d (THead (Bind Abbr) v2 t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h (s (Flat Appl) d) (THead (Bind Abst) u t3)
THead
Bind Abst
lift h (s (Flat Appl) d) u
lift h (s (Bind Abst) (s (Flat Appl) d)) t3
end of h2
by (eq_ind_r . . . h1 . h2)
pr0
THead
Flat Appl
lift h d v1
lift h (s (Flat Appl) d) (THead (Bind Abst) u t3)
lift h d (THead (Bind Abbr) v2 t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Appl) v1 (THead (Bind Abst) u t3))
THead
Flat Appl
lift h d v1
lift h (s (Flat Appl) d) (THead (Bind Abst) u t3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
pr0
lift h d (THead (Flat Appl) v1 (THead (Bind Abst) u t3))
lift h d (THead (Bind Abbr) v2 t4)
∀h:nat
.∀d:nat
.pr0
lift h d (THead (Flat Appl) v1 (THead (Bind Abst) u t3))
lift h d (THead (Bind Abbr) v2 t4)
case pr0_upsilon : b:B H0:not (eq B b Abst) v1:T v2:T :pr0 v1 v2 u1:T u2:T :pr0 u1 u2 t3:T t4:T :pr0 t3 t4 ⇒
the thesis becomes
∀h:nat
.∀d:nat
.pr0
lift h d (THead (Flat Appl) v1 (THead (Bind b) u1 t3))
lift
h
d
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
(H2) by induction hypothesis we know ∀h:nat.∀d:nat.(pr0 (lift h d v1) (lift h d v2))
(H4) by induction hypothesis we know ∀h:nat.∀d:nat.(pr0 (lift h d u1) (lift h d u2))
(H6) by induction hypothesis we know ∀h:nat.∀d:nat.(pr0 (lift h d t3) (lift h d t4))
assume h: nat
assume d: nat
(h1)
(h1)
(h1)
(h1)
by (refl_equal . .)
we proved eq nat (S d) (S d)
that is equivalent to eq nat (plus (S O) d) (S d)
we proceed by induction on the previous result to prove
pr0
THead
Flat Appl
lift h d v1
THead (Bind b) (lift h d u1) (lift h (S d) t3)
THead
Bind b
lift h d u2
THead
Flat Appl
lift h (S d) (lift (S O) O v2)
lift h (S d) t4
case refl_equal : ⇒
the thesis becomes
pr0
THead
Flat Appl
lift h d v1
THead (Bind b) (lift h d u1) (lift h (plus (S O) d) t3)
THead
Bind b
lift h d u2
THead
Flat Appl
lift h (plus (S O) d) (lift (S O) O v2)
lift h (plus (S O) d) t4
(h1)
(h1)
by (H2 . .)
pr0 (lift h d v1) (lift h d v2)
end of h1
(h2)
by (H4 . .)
pr0 (lift h d u1) (lift h d u2)
end of h2
(h3)
by (H6 . .)
pr0 (lift h (plus (S O) d) t3) (lift h (plus (S O) d) t4)
end of h3
by (pr0_upsilon . H0 . . h1 . . h2 . . h3)
pr0
THead
Flat Appl
lift h d v1
THead (Bind b) (lift h d u1) (lift h (plus (S O) d) t3)
THead
Bind b
lift h d u2
THead
Flat Appl
lift (S O) O (lift h d v2)
lift h (plus (S O) d) t4
end of h1
(h2)
by (le_O_n .)
we proved le O d
by (lift_d . . . . . previous)
eq
T
lift h (plus (S O) d) (lift (S O) O v2)
lift (S O) O (lift h d v2)
end of h2
by (eq_ind_r . . . h1 . h2)
pr0
THead
Flat Appl
lift h d v1
THead (Bind b) (lift h d u1) (lift h (plus (S O) d) t3)
THead
Bind b
lift h d u2
THead
Flat Appl
lift h (plus (S O) d) (lift (S O) O v2)
lift h (plus (S O) d) t4
we proved
pr0
THead
Flat Appl
lift h d v1
THead (Bind b) (lift h d u1) (lift h (S d) t3)
THead
Bind b
lift h d u2
THead
Flat Appl
lift h (S d) (lift (S O) O v2)
lift h (S d) t4
pr0
THead
Flat Appl
lift h d v1
THead
Bind b
lift h (s (Flat Appl) d) u1
lift h (s (Bind b) (s (Flat Appl) d)) t3
THead
Bind b
lift h d u2
THead
Flat Appl
lift h (s (Bind b) d) (lift (S O) O v2)
lift h (s (Flat Appl) (s (Bind b) d)) t4
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h (s (Bind b) d) (THead (Flat Appl) (lift (S O) O v2) t4)
THead
Flat Appl
lift h (s (Bind b) d) (lift (S O) O v2)
lift h (s (Flat Appl) (s (Bind b) d)) t4
end of h2
by (eq_ind_r . . . h1 . h2)
pr0
THead
Flat Appl
lift h d v1
THead
Bind b
lift h (s (Flat Appl) d) u1
lift h (s (Bind b) (s (Flat Appl) d)) t3
THead
Bind b
lift h d u2
lift h (s (Bind b) d) (THead (Flat Appl) (lift (S O) O v2) t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift
h
d
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead
Bind b
lift h d u2
lift h (s (Bind b) d) (THead (Flat Appl) (lift (S O) O v2) t4)
end of h2
by (eq_ind_r . . . h1 . h2)
pr0
THead
Flat Appl
lift h d v1
THead
Bind b
lift h (s (Flat Appl) d) u1
lift h (s (Bind b) (s (Flat Appl) d)) t3
lift
h
d
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h (s (Flat Appl) d) (THead (Bind b) u1 t3)
THead
Bind b
lift h (s (Flat Appl) d) u1
lift h (s (Bind b) (s (Flat Appl) d)) t3
end of h2
by (eq_ind_r . . . h1 . h2)
pr0
THead
Flat Appl
lift h d v1
lift h (s (Flat Appl) d) (THead (Bind b) u1 t3)
lift
h
d
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Appl) v1 (THead (Bind b) u1 t3))
THead
Flat Appl
lift h d v1
lift h (s (Flat Appl) d) (THead (Bind b) u1 t3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
pr0
lift h d (THead (Flat Appl) v1 (THead (Bind b) u1 t3))
lift
h
d
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
∀h:nat
.∀d:nat
.pr0
lift h d (THead (Flat Appl) v1 (THead (Bind b) u1 t3))
lift
h
d
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
case pr0_delta : u1:T u2:T :pr0 u1 u2 t3:T t4:T :pr0 t3 t4 w:T H4:subst0 O u2 t4 w ⇒
the thesis becomes
∀h:nat
.∀d:nat
.pr0
lift h d (THead (Bind Abbr) u1 t3)
lift h d (THead (Bind Abbr) u2 w)
(H1) by induction hypothesis we know ∀h:nat.∀d:nat.(pr0 (lift h d u1) (lift h d u2))
(H3) by induction hypothesis we know ∀h:nat.∀d:nat.(pr0 (lift h d t3) (lift h d t4))
assume h: nat
assume d: nat
(h1)
(h1)
(h1)
by (H1 . .)
pr0 (lift h d u1) (lift h d u2)
end of h1
(h2)
by (H3 . .)
pr0 (lift h (S d) t3) (lift h (S d) t4)
end of h2
(h3)
(d') by (. .) we proved
by (minus_n_O .)
we proved eq nat d (minus d O)
we proceed by induction on the previous result to prove eq nat (minus d O) d
case refl_equal : ⇒
the thesis becomes eq nat d d
by (refl_equal . .)
eq nat d d
we proved eq nat (minus d O) d
that is equivalent to eq nat (minus (S d) (S O)) d
we proceed by induction on the previous result to prove subst0 O (lift h d u2) (lift h d' t4) (lift h d' w)
case refl_equal : ⇒
the thesis becomes subst0 O (lift h (minus (S d) (S O)) u2) (lift h d' t4) (lift h d' w)
by (le_O_n .)
we proved le O d
by (le_n_S . . previous)
we proved le (S O) (S d)
that is equivalent to lt O (S d)
by (subst0_lift_lt . . . . H4 . previous .)
we proved
subst0
O
lift h (minus (S d) (S O)) u2
lift h (S d) t4
lift h (S d) w
subst0 O (lift h (minus (S d) (S O)) u2) (lift h d' t4) (lift h d' w)
we proved let d' := S d
in subst0 O (lift h d u2) (lift h d' t4) (lift h d' w)
subst0 O (lift h d u2) (lift h (S d) t4) (lift h (S d) w)
end of h3
by (pr0_delta . . h1 . . h2 . h3)
we proved
pr0
THead (Bind Abbr) (lift h d u1) (lift h (S d) t3)
THead (Bind Abbr) (lift h d u2) (lift h (S d) w)
pr0
THead (Bind Abbr) (lift h d u1) (lift h (s (Bind Abbr) d) t3)
THead (Bind Abbr) (lift h d u2) (lift h (s (Bind Abbr) d) w)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Bind Abbr) u2 w)
THead (Bind Abbr) (lift h d u2) (lift h (s (Bind Abbr) d) w)
end of h2
by (eq_ind_r . . . h1 . h2)
pr0
THead (Bind Abbr) (lift h d u1) (lift h (s (Bind Abbr) d) t3)
lift h d (THead (Bind Abbr) u2 w)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Bind Abbr) u1 t3)
THead (Bind Abbr) (lift h d u1) (lift h (s (Bind Abbr) d) t3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
pr0
lift h d (THead (Bind Abbr) u1 t3)
lift h d (THead (Bind Abbr) u2 w)
∀h:nat
.∀d:nat
.pr0
lift h d (THead (Bind Abbr) u1 t3)
lift h d (THead (Bind Abbr) u2 w)
case pr0_zeta : b:B H0:not (eq B b Abst) t3:T t4:T :pr0 t3 t4 u:T ⇒
the thesis becomes
∀h:nat
.∀d:nat.(pr0 (lift h d (THead (Bind b) u (lift (S O) O t3))) (lift h d t4))
(H2) by induction hypothesis we know ∀h:nat.∀d:nat.(pr0 (lift h d t3) (lift h d t4))
assume h: nat
assume d: nat
(h1)
by (refl_equal . .)
we proved eq nat (S d) (S d)
that is equivalent to eq nat (plus (S O) d) (S d)
we proceed by induction on the previous result to prove
pr0
THead (Bind b) (lift h d u) (lift h (S d) (lift (S O) O t3))
lift h d t4
case refl_equal : ⇒
the thesis becomes
pr0
THead
Bind b
lift h d u
lift h (plus (S O) d) (lift (S O) O t3)
lift h d t4
(h1)
by (H2 . .)
we proved pr0 (lift h d t3) (lift h d t4)
by (pr0_zeta . H0 . . previous .)
pr0
THead (Bind b) (lift h d u) (lift (S O) O (lift h d t3))
lift h d t4
end of h1
(h2)
by (le_O_n .)
we proved le O d
by (lift_d . . . . . previous)
eq
T
lift h (plus (S O) d) (lift (S O) O t3)
lift (S O) O (lift h d t3)
end of h2
by (eq_ind_r . . . h1 . h2)
pr0
THead
Bind b
lift h d u
lift h (plus (S O) d) (lift (S O) O t3)
lift h d t4
we proved
pr0
THead (Bind b) (lift h d u) (lift h (S d) (lift (S O) O t3))
lift h d t4
pr0
THead
Bind b
lift h d u
lift h (s (Bind b) d) (lift (S O) O t3)
lift h d t4
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Bind b) u (lift (S O) O t3))
THead
Bind b
lift h d u
lift h (s (Bind b) d) (lift (S O) O t3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved pr0 (lift h d (THead (Bind b) u (lift (S O) O t3))) (lift h d t4)
∀h:nat
.∀d:nat.(pr0 (lift h d (THead (Bind b) u (lift (S O) O t3))) (lift h d t4))
case pr0_tau : t3:T t4:T :pr0 t3 t4 u:T ⇒
the thesis becomes ∀h:nat.∀d:nat.(pr0 (lift h d (THead (Flat Cast) u t3)) (lift h d t4))
(H1) by induction hypothesis we know ∀h:nat.∀d:nat.(pr0 (lift h d t3) (lift h d t4))
assume h: nat
assume d: nat
(h1)
by (H1 . .)
we proved pr0 (lift h d t3) (lift h d t4)
that is equivalent to pr0 (lift h (s (Flat Cast) d) t3) (lift h d t4)
by (pr0_tau . . previous .)
pr0
THead (Flat Cast) (lift h d u) (lift h (s (Flat Cast) d) t3)
lift h d t4
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Cast) u t3)
THead (Flat Cast) (lift h d u) (lift h (s (Flat Cast) d) t3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved pr0 (lift h d (THead (Flat Cast) u t3)) (lift h d t4)
∀h:nat.∀d:nat.(pr0 (lift h d (THead (Flat Cast) u t3)) (lift h d t4))
we proved ∀h:nat.∀d:nat.(pr0 (lift h d t1) (lift h d t2))
we proved ∀t1:T.∀t2:T.(pr0 t1 t2)→∀h:nat.∀d:nat.(pr0 (lift h d t1) (lift h d t2))