DEFINITION arity_gen_lift()
TYPE =
∀g:G
.∀c1:C
.∀t:T
.∀a:A
.∀h:nat
.∀d:nat.(arity g c1 (lift h d t) a)→∀c2:C.(drop h d c1 c2)→(arity g c2 t a)
BODY =
assume g: G
assume c1: C
assume t: T
assume a: A
assume h: nat
assume d: nat
suppose H: arity g c1 (lift h d t) a
assume y: T
suppose H0: arity g c1 y a
we proceed by induction on H0 to prove ∀x:nat.∀x0:T.(eq T y (lift h x x0))→∀c2:C.(drop h x c1 c2)→(arity g c2 x0 a)
case arity_sort : c:C n:nat ⇒
the thesis becomes
∀x:nat
.∀x0:T
.∀H1:eq T (TSort n) (lift h x x0)
.∀c2:C.(drop h x c c2)→(arity g c2 x0 (ASort O n))
assume x: nat
assume x0: T
suppose H1: eq T (TSort n) (lift h x x0)
assume c2: C
suppose : drop h x c c2
(h1)
by (arity_sort . . .)
arity g c2 (TSort n) (ASort O n)
end of h1
(h2)
by (lift_gen_sort . . . . H1)
eq T x0 (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c2 x0 (ASort O n)
∀x:nat
.∀x0:T
.∀H1:eq T (TSort n) (lift h x x0)
.∀c2:C.(drop h x c c2)→(arity g c2 x0 (ASort O n))
case arity_abbr : c:C d0:C u:T i:nat H1:getl i c (CHead d0 (Bind Abbr) u) a0:A H2:arity g d0 u a0 ⇒
the thesis becomes ∀x:nat.∀x0:T.∀H4:(eq T (TLRef i) (lift h x x0)).∀c2:C.∀H5:(drop h x c c2).(arity g c2 x0 a0)
(H3) by induction hypothesis we know ∀x:nat.∀x0:T.(eq T u (lift h x x0))→∀c2:C.(drop h x d0 c2)→(arity g c2 x0 a0)
assume x: nat
assume x0: T
suppose H4: eq T (TLRef i) (lift h x x0)
assume c2: C
suppose H5: drop h x c c2
(H_x)
by (lift_gen_lref . . . . H4)
or
land (lt i x) (eq T x0 (TLRef i))
land (le (plus x h) i) (eq T x0 (TLRef (minus i h)))
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove arity g c2 x0 a0
case or_introl : H7:land (lt i x) (eq T x0 (TLRef i)) ⇒
the thesis becomes arity g c2 x0 a0
we proceed by induction on H7 to prove arity g c2 x0 a0
case conj : H8:lt i x H9:eq T x0 (TLRef i) ⇒
the thesis becomes arity g c2 x0 a0
(H10)
by (lt_plus_minus . . H8)
we proved eq nat x (S (plus i (minus x (S i))))
we proceed by induction on the previous result to prove drop h (S (plus i (minus x (S i)))) c c2
case refl_equal : ⇒
the thesis becomes the hypothesis H5
drop h (S (plus i (minus x (S i)))) c c2
end of H10
by (getl_drop_conf_lt . . . . . H1 . . . H10)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (minus x (S i)) v)
λv:T.λe0:C.getl i c2 (CHead e0 (Bind Abbr) v)
λ:T.λe0:C.drop h (minus x (S i)) d0 e0
we proceed by induction on the previous result to prove arity g c2 (TLRef i) a0
case ex3_2_intro : x1:T x2:C H11:eq T u (lift h (minus x (S i)) x1) H12:getl i c2 (CHead x2 (Bind Abbr) x1) H13:drop h (minus x (S i)) d0 x2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H14)
we proceed by induction on H11 to prove
∀x3:nat
.∀x4:T
.eq T (lift h (minus x (S i)) x1) (lift h x3 x4)
→∀c3:C.(drop h x3 d0 c3)→(arity g c3 x4 a0)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀x3:nat
.∀x4:T
.eq T (lift h (minus x (S i)) x1) (lift h x3 x4)
→∀c3:C.(drop h x3 d0 c3)→(arity g c3 x4 a0)
end of H14
by (refl_equal . .)
we proved eq T (lift h (minus x (S i)) x1) (lift h (minus x (S i)) x1)
by (H14 . . previous . H13)
we proved arity g x2 x1 a0
by (arity_abbr . . . . . H12 . previous)
arity g c2 (TLRef i) a0
we proved arity g c2 (TLRef i) a0
by (eq_ind_r . . . previous . H9)
arity g c2 x0 a0
arity g c2 x0 a0
case or_intror : H7:land (le (plus x h) i) (eq T x0 (TLRef (minus i h))) ⇒
the thesis becomes arity g c2 x0 a0
we proceed by induction on H7 to prove arity g c2 x0 a0
case conj : H8:le (plus x h) i H9:eq T x0 (TLRef (minus i h)) ⇒
the thesis becomes arity g c2 x0 a0
by (getl_drop_conf_ge . . . H1 . . . H5 H8)
we proved getl (minus i h) c2 (CHead d0 (Bind Abbr) u)
by (arity_abbr . . . . . previous . H2)
we proved arity g c2 (TLRef (minus i h)) a0
by (eq_ind_r . . . previous . H9)
arity g c2 x0 a0
arity g c2 x0 a0
we proved arity g c2 x0 a0
∀x:nat.∀x0:T.∀H4:(eq T (TLRef i) (lift h x x0)).∀c2:C.∀H5:(drop h x c c2).(arity g c2 x0 a0)
case arity_abst : c:C d0:C u:T i:nat H1:getl i c (CHead d0 (Bind Abst) u) a0:A H2:arity g d0 u (asucc g a0) ⇒
the thesis becomes ∀x:nat.∀x0:T.∀H4:(eq T (TLRef i) (lift h x x0)).∀c2:C.∀H5:(drop h x c c2).(arity g c2 x0 a0)
(H3) by induction hypothesis we know
∀x:nat
.∀x0:T.(eq T u (lift h x x0))→∀c2:C.(drop h x d0 c2)→(arity g c2 x0 (asucc g a0))
assume x: nat
assume x0: T
suppose H4: eq T (TLRef i) (lift h x x0)
assume c2: C
suppose H5: drop h x c c2
(H_x)
by (lift_gen_lref . . . . H4)
or
land (lt i x) (eq T x0 (TLRef i))
land (le (plus x h) i) (eq T x0 (TLRef (minus i h)))
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove arity g c2 x0 a0
case or_introl : H7:land (lt i x) (eq T x0 (TLRef i)) ⇒
the thesis becomes arity g c2 x0 a0
we proceed by induction on H7 to prove arity g c2 x0 a0
case conj : H8:lt i x H9:eq T x0 (TLRef i) ⇒
the thesis becomes arity g c2 x0 a0
(H10)
by (lt_plus_minus . . H8)
we proved eq nat x (S (plus i (minus x (S i))))
we proceed by induction on the previous result to prove drop h (S (plus i (minus x (S i)))) c c2
case refl_equal : ⇒
the thesis becomes the hypothesis H5
drop h (S (plus i (minus x (S i)))) c c2
end of H10
by (getl_drop_conf_lt . . . . . H1 . . . H10)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (minus x (S i)) v)
λv:T.λe0:C.getl i c2 (CHead e0 (Bind Abst) v)
λ:T.λe0:C.drop h (minus x (S i)) d0 e0
we proceed by induction on the previous result to prove arity g c2 (TLRef i) a0
case ex3_2_intro : x1:T x2:C H11:eq T u (lift h (minus x (S i)) x1) H12:getl i c2 (CHead x2 (Bind Abst) x1) H13:drop h (minus x (S i)) d0 x2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H14)
we proceed by induction on H11 to prove
∀x3:nat
.∀x4:T
.eq T (lift h (minus x (S i)) x1) (lift h x3 x4)
→∀c3:C.(drop h x3 d0 c3)→(arity g c3 x4 (asucc g a0))
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀x3:nat
.∀x4:T
.eq T (lift h (minus x (S i)) x1) (lift h x3 x4)
→∀c3:C.(drop h x3 d0 c3)→(arity g c3 x4 (asucc g a0))
end of H14
by (refl_equal . .)
we proved eq T (lift h (minus x (S i)) x1) (lift h (minus x (S i)) x1)
by (H14 . . previous . H13)
we proved arity g x2 x1 (asucc g a0)
by (arity_abst . . . . . H12 . previous)
arity g c2 (TLRef i) a0
we proved arity g c2 (TLRef i) a0
by (eq_ind_r . . . previous . H9)
arity g c2 x0 a0
arity g c2 x0 a0
case or_intror : H7:land (le (plus x h) i) (eq T x0 (TLRef (minus i h))) ⇒
the thesis becomes arity g c2 x0 a0
we proceed by induction on H7 to prove arity g c2 x0 a0
case conj : H8:le (plus x h) i H9:eq T x0 (TLRef (minus i h)) ⇒
the thesis becomes arity g c2 x0 a0
by (getl_drop_conf_ge . . . H1 . . . H5 H8)
we proved getl (minus i h) c2 (CHead d0 (Bind Abst) u)
by (arity_abst . . . . . previous . H2)
we proved arity g c2 (TLRef (minus i h)) a0
by (eq_ind_r . . . previous . H9)
arity g c2 x0 a0
arity g c2 x0 a0
we proved arity g c2 x0 a0
∀x:nat.∀x0:T.∀H4:(eq T (TLRef i) (lift h x x0)).∀c2:C.∀H5:(drop h x c c2).(arity g c2 x0 a0)
case arity_bind : b:B H1:not (eq B b Abst) c:C u:T a1:A H2:arity g c u a1 t0:T a2:A H4:arity g (CHead c (Bind b) u) t0 a2 ⇒
the thesis becomes
∀x:nat
.∀x0:T.∀H6:(eq T (THead (Bind b) u t0) (lift h x x0)).∀c2:C.∀H7:(drop h x c c2).(arity g c2 x0 a2)
(H3) by induction hypothesis we know ∀x:nat.∀x0:T.(eq T u (lift h x x0))→∀c2:C.(drop h x c c2)→(arity g c2 x0 a1)
(H5) by induction hypothesis we know
∀x:nat
.∀x0:T
.eq T t0 (lift h x x0)
→∀c2:C.(drop h x (CHead c (Bind b) u) c2)→(arity g c2 x0 a2)
assume x: nat
assume x0: T
suppose H6: eq T (THead (Bind b) u t0) (lift h x x0)
assume c2: C
suppose H7: drop h x c c2
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 u (lift h x y)
λ:T.λz:T.eq T t0 (lift h (S x) z)
we proceed by induction on the previous result to prove arity g c2 x0 a2
case ex3_2_intro : x1:T x2:T H8:eq T x0 (THead (Bind b) x1 x2) H9:eq T u (lift h x x1) H10:eq T t0 (lift h (S x) x2) ⇒
the thesis becomes arity g c2 x0 a2
(H11)
we proceed by induction on H10 to prove
∀x3:nat
.∀x4:T
.eq T (lift h (S x) x2) (lift h x3 x4)
→∀c3:C.(drop h x3 (CHead c (Bind b) u) c3)→(arity g c3 x4 a2)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
∀x3:nat
.∀x4:T
.eq T (lift h (S x) x2) (lift h x3 x4)
→∀c3:C.(drop h x3 (CHead c (Bind b) u) c3)→(arity g c3 x4 a2)
end of H11
(H12)
we proceed by induction on H10 to prove arity g (CHead c (Bind b) u) (lift h (S x) x2) a2
case refl_equal : ⇒
the thesis becomes the hypothesis H4
arity g (CHead c (Bind b) u) (lift h (S x) x2) a2
end of H12
(H14)
we proceed by induction on H9 to prove
∀x3:nat
.∀x4:T
.eq T (lift h (S x) x2) (lift h x3 x4)
→∀c3:C.(drop h x3 (CHead c (Bind b) (lift h x x1)) c3)→(arity g c3 x4 a2)
case refl_equal : ⇒
the thesis becomes the hypothesis H11
∀x3:nat
.∀x4:T
.eq T (lift h (S x) x2) (lift h x3 x4)
→∀c3:C.(drop h x3 (CHead c (Bind b) (lift h x x1)) c3)→(arity g c3 x4 a2)
end of H14
(H15)
we proceed by induction on H9 to prove
∀x3:nat
.∀x4:T.(eq T (lift h x x1) (lift h x3 x4))→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 a1)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀x3:nat
.∀x4:T.(eq T (lift h x x1) (lift h x3 x4))→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 a1)
end of H15
(h1)
by (refl_equal . .)
we proved eq T (lift h x x1) (lift h x x1)
by (H15 . . previous . H7)
arity g c2 x1 a1
end of h1
(h2)
(h1)
by (refl_equal . .)
eq T (lift h (S x) x2) (lift h (S x) x2)
end of h1
(h2)
by (drop_skip_bind . . . . H7 . .)
drop h (S x) (CHead c (Bind b) (lift h x x1)) (CHead c2 (Bind b) x1)
end of h2
by (H14 . . h1 . h2)
arity g (CHead c2 (Bind b) x1) x2 a2
end of h2
by (arity_bind . . H1 . . . h1 . . h2)
we proved arity g c2 (THead (Bind b) x1 x2) a2
by (eq_ind_r . . . previous . H8)
arity g c2 x0 a2
we proved arity g c2 x0 a2
∀x:nat
.∀x0:T.∀H6:(eq T (THead (Bind b) u t0) (lift h x x0)).∀c2:C.∀H7:(drop h x c c2).(arity g c2 x0 a2)
case arity_head : c:C u:T a1:A H1:arity g c u (asucc g a1) t0:T a2:A H3:arity g (CHead c (Bind Abst) u) t0 a2 ⇒
the thesis becomes
∀x:nat
.∀x0:T
.∀H5:eq T (THead (Bind Abst) u t0) (lift h x x0)
.∀c2:C.∀H6:(drop h x c c2).(arity g c2 x0 (AHead a1 a2))
(H2) by induction hypothesis we know
∀x:nat
.∀x0:T
.(eq T u (lift h x x0))→∀c2:C.(drop h x c c2)→(arity g c2 x0 (asucc g a1))
(H4) by induction hypothesis we know
∀x:nat
.∀x0:T
.eq T t0 (lift h x x0)
→∀c2:C.(drop h x (CHead c (Bind Abst) u) c2)→(arity g c2 x0 a2)
assume x: nat
assume x0: T
suppose H5: eq T (THead (Bind Abst) u t0) (lift h x x0)
assume c2: C
suppose H6: drop h x c c2
by (lift_gen_bind . . . . . . H5)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Bind Abst) y z)
λy:T.λ:T.eq T u (lift h x y)
λ:T.λz:T.eq T t0 (lift h (S x) z)
we proceed by induction on the previous result to prove arity g c2 x0 (AHead a1 a2)
case ex3_2_intro : x1:T x2:T H7:eq T x0 (THead (Bind Abst) x1 x2) H8:eq T u (lift h x x1) H9:eq T t0 (lift h (S x) x2) ⇒
the thesis becomes arity g c2 x0 (AHead a1 a2)
(H10)
we proceed by induction on H9 to prove
∀x3:nat
.∀x4:T
.eq T (lift h (S x) x2) (lift h x3 x4)
→∀c3:C.(drop h x3 (CHead c (Bind Abst) u) c3)→(arity g c3 x4 a2)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
∀x3:nat
.∀x4:T
.eq T (lift h (S x) x2) (lift h x3 x4)
→∀c3:C.(drop h x3 (CHead c (Bind Abst) u) c3)→(arity g c3 x4 a2)
end of H10
(H11)
we proceed by induction on H9 to prove arity g (CHead c (Bind Abst) u) (lift h (S x) x2) a2
case refl_equal : ⇒
the thesis becomes the hypothesis H3
arity g (CHead c (Bind Abst) u) (lift h (S x) x2) a2
end of H11
(H13)
we proceed by induction on H8 to prove
∀x3:nat
.∀x4:T
.eq T (lift h (S x) x2) (lift h x3 x4)
→∀c3:C.(drop h x3 (CHead c (Bind Abst) (lift h x x1)) c3)→(arity g c3 x4 a2)
case refl_equal : ⇒
the thesis becomes the hypothesis H10
∀x3:nat
.∀x4:T
.eq T (lift h (S x) x2) (lift h x3 x4)
→∀c3:C.(drop h x3 (CHead c (Bind Abst) (lift h x x1)) c3)→(arity g c3 x4 a2)
end of H13
(H14)
we proceed by induction on H8 to prove
∀x3:nat
.∀x4:T
.eq T (lift h x x1) (lift h x3 x4)
→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 (asucc g a1))
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀x3:nat
.∀x4:T
.eq T (lift h x x1) (lift h x3 x4)
→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 (asucc g a1))
end of H14
(h1)
by (refl_equal . .)
we proved eq T (lift h x x1) (lift h x x1)
by (H14 . . previous . H6)
arity g c2 x1 (asucc g a1)
end of h1
(h2)
(h1)
by (refl_equal . .)
eq T (lift h (S x) x2) (lift h (S x) x2)
end of h1
(h2)
by (drop_skip_bind . . . . H6 . .)
drop
h
S x
CHead c (Bind Abst) (lift h x x1)
CHead c2 (Bind Abst) x1
end of h2
by (H13 . . h1 . h2)
arity g (CHead c2 (Bind Abst) x1) x2 a2
end of h2
by (arity_head . . . . h1 . . h2)
we proved arity g c2 (THead (Bind Abst) x1 x2) (AHead a1 a2)
by (eq_ind_r . . . previous . H7)
arity g c2 x0 (AHead a1 a2)
we proved arity g c2 x0 (AHead a1 a2)
∀x:nat
.∀x0:T
.∀H5:eq T (THead (Bind Abst) u t0) (lift h x x0)
.∀c2:C.∀H6:(drop h x c c2).(arity g c2 x0 (AHead a1 a2))
case arity_appl : c:C u:T a1:A H1:arity g c u a1 t0:T a2:A H3:arity g c t0 (AHead a1 a2) ⇒
the thesis becomes
∀x:nat
.∀x0:T
.∀H5:(eq T (THead (Flat Appl) u t0) (lift h x x0)).∀c2:C.∀H6:(drop h x c c2).(arity g c2 x0 a2)
(H2) by induction hypothesis we know ∀x:nat.∀x0:T.(eq T u (lift h x x0))→∀c2:C.(drop h x c c2)→(arity g c2 x0 a1)
(H4) by induction hypothesis we know
∀x:nat
.∀x0:T.(eq T t0 (lift h x x0))→∀c2:C.(drop h x c c2)→(arity g c2 x0 (AHead a1 a2))
assume x: nat
assume x0: T
suppose H5: eq T (THead (Flat Appl) u t0) (lift h x x0)
assume c2: C
suppose H6: drop h x c c2
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 u (lift h x y)
λ:T.λz:T.eq T t0 (lift h x z)
we proceed by induction on the previous result to prove arity g c2 x0 a2
case ex3_2_intro : x1:T x2:T H7:eq T x0 (THead (Flat Appl) x1 x2) H8:eq T u (lift h x x1) H9:eq T t0 (lift h x x2) ⇒
the thesis becomes arity g c2 x0 a2
(H10)
we proceed by induction on H9 to prove
∀x3:nat
.∀x4:T
.eq T (lift h x x2) (lift h x3 x4)
→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 (AHead a1 a2))
case refl_equal : ⇒
the thesis becomes the hypothesis H4
∀x3:nat
.∀x4:T
.eq T (lift h x x2) (lift h x3 x4)
→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 (AHead a1 a2))
end of H10
(H12)
we proceed by induction on H8 to prove
∀x3:nat
.∀x4:T.(eq T (lift h x x1) (lift h x3 x4))→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 a1)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀x3:nat
.∀x4:T.(eq T (lift h x x1) (lift h x3 x4))→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 a1)
end of H12
(h1)
by (refl_equal . .)
we proved eq T (lift h x x1) (lift h x x1)
by (H12 . . previous . H6)
arity g c2 x1 a1
end of h1
(h2)
by (refl_equal . .)
we proved eq T (lift h x x2) (lift h x x2)
by (H10 . . previous . H6)
arity g c2 x2 (AHead a1 a2)
end of h2
by (arity_appl . . . . h1 . . h2)
we proved arity g c2 (THead (Flat Appl) x1 x2) a2
by (eq_ind_r . . . previous . H7)
arity g c2 x0 a2
we proved arity g c2 x0 a2
∀x:nat
.∀x0:T
.∀H5:(eq T (THead (Flat Appl) u t0) (lift h x x0)).∀c2:C.∀H6:(drop h x c c2).(arity g c2 x0 a2)
case arity_cast : c:C u:T a0:A H1:arity g c u (asucc g a0) t0:T H3:arity g c t0 a0 ⇒
the thesis becomes
∀x:nat
.∀x0:T
.∀H5:(eq T (THead (Flat Cast) u t0) (lift h x x0)).∀c2:C.∀H6:(drop h x c c2).(arity g c2 x0 a0)
(H2) by induction hypothesis we know
∀x:nat
.∀x0:T
.(eq T u (lift h x x0))→∀c2:C.(drop h x c c2)→(arity g c2 x0 (asucc g a0))
(H4) by induction hypothesis we know ∀x:nat.∀x0:T.(eq T t0 (lift h x x0))→∀c2:C.(drop h x c c2)→(arity g c2 x0 a0)
assume x: nat
assume x0: T
suppose H5: eq T (THead (Flat Cast) u t0) (lift h x x0)
assume c2: C
suppose H6: drop h x c c2
by (lift_gen_flat . . . . . . H5)
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 x y)
λ:T.λz:T.eq T t0 (lift h x z)
we proceed by induction on the previous result to prove arity g c2 x0 a0
case ex3_2_intro : x1:T x2:T H7:eq T x0 (THead (Flat Cast) x1 x2) H8:eq T u (lift h x x1) H9:eq T t0 (lift h x x2) ⇒
the thesis becomes arity g c2 x0 a0
(H10)
we proceed by induction on H9 to prove
∀x3:nat
.∀x4:T.(eq T (lift h x x2) (lift h x3 x4))→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 a0)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
∀x3:nat
.∀x4:T.(eq T (lift h x x2) (lift h x3 x4))→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 a0)
end of H10
(H12)
we proceed by induction on H8 to prove
∀x3:nat
.∀x4:T
.eq T (lift h x x1) (lift h x3 x4)
→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 (asucc g a0))
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀x3:nat
.∀x4:T
.eq T (lift h x x1) (lift h x3 x4)
→∀c3:C.(drop h x3 c c3)→(arity g c3 x4 (asucc g a0))
end of H12
(h1)
by (refl_equal . .)
we proved eq T (lift h x x1) (lift h x x1)
by (H12 . . previous . H6)
arity g c2 x1 (asucc g a0)
end of h1
(h2)
by (refl_equal . .)
we proved eq T (lift h x x2) (lift h x x2)
by (H10 . . previous . H6)
arity g c2 x2 a0
end of h2
by (arity_cast . . . . h1 . h2)
we proved arity g c2 (THead (Flat Cast) x1 x2) a0
by (eq_ind_r . . . previous . H7)
arity g c2 x0 a0
we proved arity g c2 x0 a0
∀x:nat
.∀x0:T
.∀H5:(eq T (THead (Flat Cast) u t0) (lift h x x0)).∀c2:C.∀H6:(drop h x c c2).(arity g c2 x0 a0)
case arity_repl : c:C t0:T a1:A :arity g c t0 a1 a2:A H3:leq g a1 a2 ⇒
the thesis becomes ∀x:nat.∀x0:T.∀H4:(eq T t0 (lift h x x0)).∀c2:C.∀H5:(drop h x c c2).(arity g c2 x0 a2)
(H2) by induction hypothesis we know ∀x:nat.∀x0:T.(eq T t0 (lift h x x0))→∀c2:C.(drop h x c c2)→(arity g c2 x0 a1)
assume x: nat
assume x0: T
suppose H4: eq T t0 (lift h x x0)
assume c2: C
suppose H5: drop h x c c2
by (H2 . . H4 . H5)
we proved arity g c2 x0 a1
by (arity_repl . . . . previous . H3)
we proved arity g c2 x0 a2
∀x:nat.∀x0:T.∀H4:(eq T t0 (lift h x x0)).∀c2:C.∀H5:(drop h x c c2).(arity g c2 x0 a2)
we proved ∀x:nat.∀x0:T.(eq T y (lift h x x0))→∀c2:C.(drop h x c1 c2)→(arity g c2 x0 a)
by (unintro . . . previous)
we proved ∀x:T.(eq T y (lift h d x))→∀c2:C.(drop h d c1 c2)→(arity g c2 x a)
by (unintro . . . previous)
we proved (eq T y (lift h d t))→∀c2:C.(drop h d c1 c2)→(arity g c2 t a)
we proved
∀y:T
.arity g c1 y a
→(eq T y (lift h d t))→∀c2:C.(drop h d c1 c2)→(arity g c2 t a)
by (insert_eq . . . . previous H)
we proved ∀c2:C.(drop h d c1 c2)→(arity g c2 t a)
we proved
∀g:G
.∀c1:C
.∀t:T
.∀a:A
.∀h:nat
.∀d:nat.(arity g c1 (lift h d t) a)→∀c2:C.(drop h d c1 c2)→(arity g c2 t a)