DEFINITION arity_fsubst0()
TYPE =
∀g:G
.∀c1:C
.∀t1:T
.∀a:A
.arity g c1 t1 a
→∀d1:C
.∀u:T
.∀i:nat
.(getl i c1 (CHead d1 (Bind Abbr) u))→∀c2:C.∀t2:T.(fsubst0 i u c1 t1 c2 t2)→(arity g c2 t2 a)
BODY =
assume g: G
assume c1: C
assume t1: T
assume a: A
suppose H: arity g c1 t1 a
we proceed by induction on H to prove
∀d1:C
.∀u:T
.∀i:nat
.(getl i c1 (CHead d1 (Bind Abbr) u))→∀c2:C.∀t2:T.(fsubst0 i u c1 t1 c2 t2)→(arity g c2 t2 a)
case arity_sort : c:C n:nat ⇒
the thesis becomes
∀d1:C
.∀u:T
.∀i:nat
.getl i c (CHead d1 (Bind Abbr) u)
→∀c2:C.∀t2:T.∀H1:(fsubst0 i u c (TSort n) c2 t2).(arity g c2 t2 (ASort O n))
assume d1: C
assume u: T
assume i: nat
suppose : getl i c (CHead d1 (Bind Abbr) u)
assume c2: C
assume t2: T
suppose H1: fsubst0 i u c (TSort n) c2 t2
(H_x)
by (fsubst0_gen_base . . . . . . H1)
or3
land (eq C c c2) (subst0 i u (TSort n) t2)
land (eq T (TSort n) t2) (csubst0 i u c c2)
land (subst0 i u (TSort n) t2) (csubst0 i u c c2)
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove arity g c2 t2 (ASort O n)
case or3_intro0 : H3:land (eq C c c2) (subst0 i u (TSort n) t2) ⇒
the thesis becomes arity g c2 t2 (ASort O n)
we proceed by induction on H3 to prove arity g c2 t2 (ASort O n)
case conj : H4:eq C c c2 H5:subst0 i u (TSort n) t2 ⇒
the thesis becomes arity g c2 t2 (ASort O n)
we proceed by induction on H4 to prove arity g c2 t2 (ASort O n)
case refl_equal : ⇒
the thesis becomes arity g c t2 (ASort O n)
by (subst0_gen_sort . . . . H5 .)
arity g c t2 (ASort O n)
arity g c2 t2 (ASort O n)
arity g c2 t2 (ASort O n)
case or3_intro1 : H3:land (eq T (TSort n) t2) (csubst0 i u c c2) ⇒
the thesis becomes arity g c2 t2 (ASort O n)
we proceed by induction on H3 to prove arity g c2 t2 (ASort O n)
case conj : H4:eq T (TSort n) t2 :csubst0 i u c c2 ⇒
the thesis becomes arity g c2 t2 (ASort O n)
we proceed by induction on H4 to prove arity g c2 t2 (ASort O n)
case refl_equal : ⇒
the thesis becomes arity g c2 (TSort n) (ASort O n)
by (arity_sort . . .)
arity g c2 (TSort n) (ASort O n)
arity g c2 t2 (ASort O n)
arity g c2 t2 (ASort O n)
case or3_intro2 : H3:land (subst0 i u (TSort n) t2) (csubst0 i u c c2) ⇒
the thesis becomes arity g c2 t2 (ASort O n)
we proceed by induction on H3 to prove arity g c2 t2 (ASort O n)
case conj : H4:subst0 i u (TSort n) t2 :csubst0 i u c c2 ⇒
the thesis becomes arity g c2 t2 (ASort O n)
by (subst0_gen_sort . . . . H4 .)
arity g c2 t2 (ASort O n)
arity g c2 t2 (ASort O n)
we proved arity g c2 t2 (ASort O n)
∀d1:C
.∀u:T
.∀i:nat
.getl i c (CHead d1 (Bind Abbr) u)
→∀c2:C.∀t2:T.∀H1:(fsubst0 i u c (TSort n) c2 t2).(arity g c2 t2 (ASort O n))
case arity_abbr : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abbr) u) a0:A H1:arity g d u a0 ⇒
the thesis becomes
∀d1:C
.∀u0:T.∀i0:nat.∀H3:(getl i0 c (CHead d1 (Bind Abbr) u0)).∀c2:C.∀t2:T.∀H4:(fsubst0 i0 u0 c (TLRef i) c2 t2).(arity g c2 t2 a0)
(H2) by induction hypothesis we know
∀d1:C
.∀u0:T
.∀i0:nat
.(getl i0 d (CHead d1 (Bind Abbr) u0))→∀c2:C.∀t2:T.(fsubst0 i0 u0 d u c2 t2)→(arity g c2 t2 a0)
assume d1: C
assume u0: T
assume i0: nat
suppose H3: getl i0 c (CHead d1 (Bind Abbr) u0)
assume c2: C
assume t2: T
suppose H4: fsubst0 i0 u0 c (TLRef i) c2 t2
(H_x)
by (fsubst0_gen_base . . . . . . H4)
or3
land (eq C c c2) (subst0 i0 u0 (TLRef i) t2)
land (eq T (TLRef i) t2) (csubst0 i0 u0 c c2)
land (subst0 i0 u0 (TLRef i) t2) (csubst0 i0 u0 c c2)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove arity g c2 t2 a0
case or3_intro0 : H6:land (eq C c c2) (subst0 i0 u0 (TLRef i) t2) ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H6 to prove arity g c2 t2 a0
case conj : H7:eq C c c2 H8:subst0 i0 u0 (TLRef i) t2 ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H7 to prove arity g c2 t2 a0
case refl_equal : ⇒
the thesis becomes arity g c t2 a0
by (subst0_gen_lref . . . . H8)
we proved land (eq nat i i0) (eq T t2 (lift (S i) O u0))
we proceed by induction on the previous result to prove arity g c t2 a0
case conj : H9:eq nat i i0 H10:eq T t2 (lift (S i) O u0) ⇒
the thesis becomes arity g c t2 a0
(H11)
by (eq_ind_r . . . H3 . H9)
getl i c (CHead d1 (Bind Abbr) u0)
end of H11
(H12)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abbr) u) (CHead d1 (Bind Abbr) u0)
we proceed by induction on the previous result to prove getl i c (CHead d1 (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl i c (CHead d1 (Bind Abbr) u0)
end of H12
(H13)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abbr) u) (CHead d1 (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead d1 (Bind Abbr) u0 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d1 (Bind Abbr) u0)
end of H13
(h1)
(H14)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abbr) u) (CHead d1 (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d1 (Bind Abbr) u0 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d (Bind Abbr) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d1 (Bind Abbr) u0)
end of H14
suppose H15: eq C d d1
(H16)
consider H14
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d1 (Bind Abbr) u0 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u u0
by (eq_ind_r . . . H12 . previous)
getl i c (CHead d1 (Bind Abbr) u)
end of H16
consider H14
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d1 (Bind Abbr) u0 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u u0
we proceed by induction on the previous result to prove arity g c (lift (S i) O u0) a0
case refl_equal : ⇒
the thesis becomes arity g c (lift (S i) O u) a0
(H17)
by (eq_ind_r . . . H16 . H15)
getl i c (CHead d (Bind Abbr) u)
end of H17
by (getl_drop . . . . . H17)
we proved drop (S i) O c d
by (arity_lift . . . . H1 . . . previous)
arity g c (lift (S i) O u) a0
we proved arity g c (lift (S i) O u0) a0
(eq C d d1)→(arity g c (lift (S i) O u0) a0)
end of h1
(h2)
consider H13
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead d1 (Bind Abbr) u0 OF CSort ⇒d | CHead c0 ⇒c0
eq C d d1
end of h2
by (h1 h2)
we proved arity g c (lift (S i) O u0) a0
by (eq_ind_r . . . previous . H10)
arity g c t2 a0
arity g c t2 a0
arity g c2 t2 a0
arity g c2 t2 a0
case or3_intro1 : H6:land (eq T (TLRef i) t2) (csubst0 i0 u0 c c2) ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H6 to prove arity g c2 t2 a0
case conj : H7:eq T (TLRef i) t2 H8:csubst0 i0 u0 c c2 ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H7 to prove arity g c2 t2 a0
case refl_equal : ⇒
the thesis becomes arity g c2 (TLRef i) a0
(h1)
suppose H9: lt i i0
(H10)
by (csubst0_getl_lt . . H9 . . . H8 . H0)
or4
getl i c2 (CHead d (Bind Abbr) u)
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl i c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i0 (S i)) u0 u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl i c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl i c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i0 (S i)) u0 u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2
end of H10
we proceed by induction on H10 to prove arity g c2 (TLRef i) a0
case or4_intro0 : H11:getl i c2 (CHead d (Bind Abbr) u) ⇒
the thesis becomes arity g c2 (TLRef i) a0
by (arity_abbr . . . . . H11 . H1)
arity g c2 (TLRef i) a0
case or4_intro1 : H11:ex3_4 B C T T λb:B.λe0:C.λu1:T.λ:T.eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b) u1) λb:B.λe0:C.λ:T.λw:T.getl i c2 (CHead e0 (Bind b) w) λ:B.λ:C.λu1:T.λw:T.subst0 (minus i0 (S i)) u0 u1 w ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H11 to prove arity g c2 (TLRef i) a0
case ex3_4_intro : x0:B x1:C x2:T x3:T H12:eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H13:getl i c2 (CHead x1 (Bind x0) x3) H14:subst0 (minus i0 (S i)) u0 x2 x3 ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H15)
by (minus_x_Sy . . H9)
we proved eq nat (minus i0 i) (S (minus i0 (S i)))
we proceed by induction on the previous result to prove
getl
S (minus i0 (S i))
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i0 i
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
consider H9
we proved lt i i0
that is equivalent to le (S i) i0
by (le_S . . previous)
we proved le (S i) (S i0)
by (le_S_n . . previous)
we proved le i i0
by (getl_conf_le . . . H3 . . H0 previous)
getl
minus i0 i
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
getl
S (minus i0 (S i))
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
end of H15
(H16)
by (f_equal . . . . . H12)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x2)
end of H16
(h1)
(H17)
by (f_equal . . . . . H12)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead d (Bind Abbr) u
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead x1 (Bind x0) x2
end of H17
(h1)
(H18)
by (f_equal . . . . . H12)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d (Bind Abbr) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead x1 (Bind x0) x2)
end of H18
suppose H19: eq B Abbr x0
suppose H20: eq C d x1
(H21)
consider H18
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u x2
by (eq_ind_r . . . H14 . previous)
subst0 (minus i0 (S i)) u0 u x3
end of H21
(H22)
by (eq_ind_r . . . H13 . H20)
getl i c2 (CHead d (Bind x0) x3)
end of H22
(H23)
by (eq_ind_r . . . H22 . H19)
getl i c2 (CHead d (Bind Abbr) x3)
end of H23
(h1)
by (getl_gen_S . . . . . H15)
getl (r (Bind Abbr) (minus i0 (S i))) d (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
consider H21
we proved subst0 (minus i0 (S i)) u0 u x3
that is equivalent to subst0 (r (Bind Abbr) (minus i0 (S i))) u0 u x3
by (fsubst0_snd . . . . . previous)
fsubst0 (r (Bind Abbr) (minus i0 (S i))) u0 d u d x3
end of h2
by (H2 . . . h1 . . h2)
we proved arity g d x3 a0
by (arity_abbr . . . . . H23 . previous)
we proved arity g c2 (TLRef i) a0
(eq B Abbr x0)→(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H17
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq B Abbr x0
end of h2
by (h1 h2)
(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H16
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
case or4_intro2 : H11:ex3_4 B C C T λb:B.λe1:C.λ:C.λu1:T.eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λu1:T.getl i c2 (CHead e2 (Bind b) u1) λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H11 to prove arity g c2 (TLRef i) a0
case ex3_4_intro : x0:B x1:C x2:C x3:T H12:eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H13:getl i c2 (CHead x2 (Bind x0) x3) H14:csubst0 (minus i0 (S i)) u0 x1 x2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H15)
by (minus_x_Sy . . H9)
we proved eq nat (minus i0 i) (S (minus i0 (S i)))
we proceed by induction on the previous result to prove
getl
S (minus i0 (S i))
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i0 i
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
consider H9
we proved lt i i0
that is equivalent to le (S i) i0
by (le_S . . previous)
we proved le (S i) (S i0)
by (le_S_n . . previous)
we proved le i i0
by (getl_conf_le . . . H3 . . H0 previous)
getl
minus i0 i
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
getl
S (minus i0 (S i))
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
end of H15
(H16)
by (f_equal . . . . . H12)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x3)
end of H16
(h1)
(H17)
by (f_equal . . . . . H12)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead d (Bind Abbr) u
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead x1 (Bind x0) x3
end of H17
(h1)
(H18)
by (f_equal . . . . . H12)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d (Bind Abbr) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead x1 (Bind x0) x3)
end of H18
suppose H19: eq B Abbr x0
suppose H20: eq C d x1
(H21)
consider H18
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u x3
by (eq_ind_r . . . H13 . previous)
getl i c2 (CHead x2 (Bind x0) u)
end of H21
(H22)
by (eq_ind_r . . . H14 . H20)
csubst0 (minus i0 (S i)) u0 d x2
end of H22
(H23)
by (eq_ind_r . . . H21 . H19)
getl i c2 (CHead x2 (Bind Abbr) u)
end of H23
(h1)
by (getl_gen_S . . . . . H15)
getl (r (Bind Abbr) (minus i0 (S i))) d (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
consider H22
we proved csubst0 (minus i0 (S i)) u0 d x2
that is equivalent to csubst0 (r (Bind Abbr) (minus i0 (S i))) u0 d x2
by (fsubst0_fst . . . . . previous)
fsubst0 (r (Bind Abbr) (minus i0 (S i))) u0 d u x2 u
end of h2
by (H2 . . . h1 . . h2)
we proved arity g x2 u a0
by (arity_abbr . . . . . H23 . previous)
we proved arity g c2 (TLRef i) a0
(eq B Abbr x0)→(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H17
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq B Abbr x0
end of h2
by (h1 h2)
(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H16
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
case or4_intro3 : H11:ex4_5 B C C T T λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λ:T.λw:T.getl i c2 (CHead e2 (Bind b) w) λ:B.λ:C.λ:C.λu1:T.λw:T.subst0 (minus i0 (S i)) u0 u1 w λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H11 to prove arity g c2 (TLRef i) a0
case ex4_5_intro : x0:B x1:C x2:C x3:T x4:T H12:eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H13:getl i c2 (CHead x2 (Bind x0) x4) H14:subst0 (minus i0 (S i)) u0 x3 x4 H15:csubst0 (minus i0 (S i)) u0 x1 x2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H16)
by (minus_x_Sy . . H9)
we proved eq nat (minus i0 i) (S (minus i0 (S i)))
we proceed by induction on the previous result to prove
getl
S (minus i0 (S i))
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i0 i
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
consider H9
we proved lt i i0
that is equivalent to le (S i) i0
by (le_S . . previous)
we proved le (S i) (S i0)
by (le_S_n . . previous)
we proved le i i0
by (getl_conf_le . . . H3 . . H0 previous)
getl
minus i0 i
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
getl
S (minus i0 (S i))
CHead d (Bind Abbr) u
CHead d1 (Bind Abbr) u0
end of H16
(H17)
by (f_equal . . . . . H12)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x3)
end of H17
(h1)
(H18)
by (f_equal . . . . . H12)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead d (Bind Abbr) u
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead x1 (Bind x0) x3
end of H18
(h1)
(H19)
by (f_equal . . . . . H12)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d (Bind Abbr) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead x1 (Bind x0) x3)
end of H19
suppose H20: eq B Abbr x0
suppose H21: eq C d x1
(H22)
consider H19
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u x3
by (eq_ind_r . . . H14 . previous)
subst0 (minus i0 (S i)) u0 u x4
end of H22
(H23)
by (eq_ind_r . . . H15 . H21)
csubst0 (minus i0 (S i)) u0 d x2
end of H23
(H24)
by (eq_ind_r . . . H13 . H20)
getl i c2 (CHead x2 (Bind Abbr) x4)
end of H24
(h1)
by (getl_gen_S . . . . . H16)
getl (r (Bind Abbr) (minus i0 (S i))) d (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
(h1)
consider H22
we proved subst0 (minus i0 (S i)) u0 u x4
subst0 (r (Bind Abbr) (minus i0 (S i))) u0 u x4
end of h1
(h2)
consider H23
we proved csubst0 (minus i0 (S i)) u0 d x2
csubst0 (r (Bind Abbr) (minus i0 (S i))) u0 d x2
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (r (Bind Abbr) (minus i0 (S i))) u0 d u x2 x4
end of h2
by (H2 . . . h1 . . h2)
we proved arity g x2 x4 a0
by (arity_abbr . . . . . H24 . previous)
we proved arity g c2 (TLRef i) a0
(eq B Abbr x0)→(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H18
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq B Abbr x0
end of h2
by (h1 h2)
(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H17
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
we proved arity g c2 (TLRef i) a0
(lt i i0)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
suppose H9: le i0 i
by (csubst0_getl_ge . . H9 . . . H8 . H0)
we proved getl i c2 (CHead d (Bind Abbr) u)
by (arity_abbr . . . . . previous . H1)
we proved arity g c2 (TLRef i) a0
(le i0 i)→(arity g c2 (TLRef i) a0)
end of h2
by (lt_le_e . . . h1 h2)
arity g c2 (TLRef i) a0
arity g c2 t2 a0
arity g c2 t2 a0
case or3_intro2 : H6:land (subst0 i0 u0 (TLRef i) t2) (csubst0 i0 u0 c c2) ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H6 to prove arity g c2 t2 a0
case conj : H7:subst0 i0 u0 (TLRef i) t2 H8:csubst0 i0 u0 c c2 ⇒
the thesis becomes arity g c2 t2 a0
by (subst0_gen_lref . . . . H7)
we proved land (eq nat i i0) (eq T t2 (lift (S i) O u0))
we proceed by induction on the previous result to prove arity g c2 t2 a0
case conj : H9:eq nat i i0 H10:eq T t2 (lift (S i) O u0) ⇒
the thesis becomes arity g c2 t2 a0
(H11)
by (eq_ind_r . . . H8 . H9)
csubst0 i u0 c c2
end of H11
(H12)
by (eq_ind_r . . . H3 . H9)
getl i c (CHead d1 (Bind Abbr) u0)
end of H12
(H13)
by (getl_mono . . . H0 . H12)
we proved eq C (CHead d (Bind Abbr) u) (CHead d1 (Bind Abbr) u0)
we proceed by induction on the previous result to prove getl i c (CHead d1 (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl i c (CHead d1 (Bind Abbr) u0)
end of H13
(H14)
by (getl_mono . . . H0 . H12)
we proved eq C (CHead d (Bind Abbr) u) (CHead d1 (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead d1 (Bind Abbr) u0 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d1 (Bind Abbr) u0)
end of H14
(h1)
(H15)
by (getl_mono . . . H0 . H12)
we proved eq C (CHead d (Bind Abbr) u) (CHead d1 (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d1 (Bind Abbr) u0 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d (Bind Abbr) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d1 (Bind Abbr) u0)
end of H15
suppose H16: eq C d d1
(H17)
consider H15
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d1 (Bind Abbr) u0 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u u0
by (eq_ind_r . . . H13 . previous)
getl i c (CHead d1 (Bind Abbr) u)
end of H17
(H18)
consider H15
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d1 (Bind Abbr) u0 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u u0
by (eq_ind_r . . . H11 . previous)
csubst0 i u c c2
end of H18
consider H15
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d1 (Bind Abbr) u0 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u u0
we proceed by induction on the previous result to prove arity g c2 (lift (S i) O u0) a0
case refl_equal : ⇒
the thesis becomes arity g c2 (lift (S i) O u) a0
(H19)
by (eq_ind_r . . . H17 . H16)
getl i c (CHead d (Bind Abbr) u)
end of H19
by (le_n .)
we proved le i i
by (csubst0_getl_ge . . previous . . . H18 . H19)
we proved getl i c2 (CHead d (Bind Abbr) u)
by (getl_drop . . . . . previous)
we proved drop (S i) O c2 d
by (arity_lift . . . . H1 . . . previous)
arity g c2 (lift (S i) O u) a0
we proved arity g c2 (lift (S i) O u0) a0
(eq C d d1)→(arity g c2 (lift (S i) O u0) a0)
end of h1
(h2)
consider H14
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead d1 (Bind Abbr) u0 OF CSort ⇒d | CHead c0 ⇒c0
eq C d d1
end of h2
by (h1 h2)
we proved arity g c2 (lift (S i) O u0) a0
by (eq_ind_r . . . previous . H10)
arity g c2 t2 a0
arity g c2 t2 a0
arity g c2 t2 a0
we proved arity g c2 t2 a0
∀d1:C
.∀u0:T.∀i0:nat.∀H3:(getl i0 c (CHead d1 (Bind Abbr) u0)).∀c2:C.∀t2:T.∀H4:(fsubst0 i0 u0 c (TLRef i) c2 t2).(arity g c2 t2 a0)
case arity_abst : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abst) u) a0:A H1:arity g d u (asucc g a0) ⇒
the thesis becomes
∀d1:C
.∀u0:T.∀i0:nat.∀H3:(getl i0 c (CHead d1 (Bind Abbr) u0)).∀c2:C.∀t2:T.∀H4:(fsubst0 i0 u0 c (TLRef i) c2 t2).(arity g c2 t2 a0)
(H2) by induction hypothesis we know
∀d1:C
.∀u0:T
.∀i0:nat
.getl i0 d (CHead d1 (Bind Abbr) u0)
→∀c2:C.∀t2:T.(fsubst0 i0 u0 d u c2 t2)→(arity g c2 t2 (asucc g a0))
assume d1: C
assume u0: T
assume i0: nat
suppose H3: getl i0 c (CHead d1 (Bind Abbr) u0)
assume c2: C
assume t2: T
suppose H4: fsubst0 i0 u0 c (TLRef i) c2 t2
(H_x)
by (fsubst0_gen_base . . . . . . H4)
or3
land (eq C c c2) (subst0 i0 u0 (TLRef i) t2)
land (eq T (TLRef i) t2) (csubst0 i0 u0 c c2)
land (subst0 i0 u0 (TLRef i) t2) (csubst0 i0 u0 c c2)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove arity g c2 t2 a0
case or3_intro0 : H6:land (eq C c c2) (subst0 i0 u0 (TLRef i) t2) ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H6 to prove arity g c2 t2 a0
case conj : H7:eq C c c2 H8:subst0 i0 u0 (TLRef i) t2 ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H7 to prove arity g c2 t2 a0
case refl_equal : ⇒
the thesis becomes arity g c t2 a0
by (subst0_gen_lref . . . . H8)
we proved land (eq nat i i0) (eq T t2 (lift (S i) O u0))
we proceed by induction on the previous result to prove arity g c t2 a0
case conj : H9:eq nat i i0 H10:eq T t2 (lift (S i) O u0) ⇒
the thesis becomes arity g c t2 a0
(H11)
by (eq_ind_r . . . H3 . H9)
getl i c (CHead d1 (Bind Abbr) u0)
end of H11
(H13)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abst) u) (CHead d1 (Bind Abbr) u0)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead d1 (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead d1 (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H13
consider H13
we proved
<λ:C.Prop>
CASE CHead d1 (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove arity g c (lift (S i) O u0) a0
we proved arity g c (lift (S i) O u0) a0
by (eq_ind_r . . . previous . H10)
arity g c t2 a0
arity g c t2 a0
arity g c2 t2 a0
arity g c2 t2 a0
case or3_intro1 : H6:land (eq T (TLRef i) t2) (csubst0 i0 u0 c c2) ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H6 to prove arity g c2 t2 a0
case conj : H7:eq T (TLRef i) t2 H8:csubst0 i0 u0 c c2 ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H7 to prove arity g c2 t2 a0
case refl_equal : ⇒
the thesis becomes arity g c2 (TLRef i) a0
(h1)
suppose H9: lt i i0
(H10)
by (csubst0_getl_lt . . H9 . . . H8 . H0)
or4
getl i c2 (CHead d (Bind Abst) u)
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead d (Bind Abst) u) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl i c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i0 (S i)) u0 u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl i c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl i c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i0 (S i)) u0 u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2
end of H10
we proceed by induction on H10 to prove arity g c2 (TLRef i) a0
case or4_intro0 : H11:getl i c2 (CHead d (Bind Abst) u) ⇒
the thesis becomes arity g c2 (TLRef i) a0
by (arity_abst . . . . . H11 . H1)
arity g c2 (TLRef i) a0
case or4_intro1 : H11:ex3_4 B C T T λb:B.λe0:C.λu1:T.λ:T.eq C (CHead d (Bind Abst) u) (CHead e0 (Bind b) u1) λb:B.λe0:C.λ:T.λw:T.getl i c2 (CHead e0 (Bind b) w) λ:B.λ:C.λu1:T.λw:T.subst0 (minus i0 (S i)) u0 u1 w ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H11 to prove arity g c2 (TLRef i) a0
case ex3_4_intro : x0:B x1:C x2:T x3:T H12:eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x2) H13:getl i c2 (CHead x1 (Bind x0) x3) H14:subst0 (minus i0 (S i)) u0 x2 x3 ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H15)
by (minus_x_Sy . . H9)
we proved eq nat (minus i0 i) (S (minus i0 (S i)))
we proceed by induction on the previous result to prove
getl
S (minus i0 (S i))
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i0 i
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
consider H9
we proved lt i i0
that is equivalent to le (S i) i0
by (le_S . . previous)
we proved le (S i) (S i0)
by (le_S_n . . previous)
we proved le i i0
by (getl_conf_le . . . H3 . . H0 previous)
getl
minus i0 i
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
getl
S (minus i0 (S i))
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
end of H15
(H16)
by (f_equal . . . . . H12)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abst) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x2)
end of H16
(h1)
(H17)
by (f_equal . . . . . H12)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead d (Bind Abst) u
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead x1 (Bind x0) x2
end of H17
(h1)
(H18)
by (f_equal . . . . . H12)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d (Bind Abst) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead x1 (Bind x0) x2)
end of H18
suppose H19: eq B Abst x0
suppose H20: eq C d x1
(H21)
consider H18
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u x2
by (eq_ind_r . . . H14 . previous)
subst0 (minus i0 (S i)) u0 u x3
end of H21
(H22)
by (eq_ind_r . . . H13 . H20)
getl i c2 (CHead d (Bind x0) x3)
end of H22
(H23)
by (eq_ind_r . . . H22 . H19)
getl i c2 (CHead d (Bind Abst) x3)
end of H23
(h1)
by (getl_gen_S . . . . . H15)
getl (r (Bind Abst) (minus i0 (S i))) d (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
consider H21
we proved subst0 (minus i0 (S i)) u0 u x3
that is equivalent to subst0 (r (Bind Abst) (minus i0 (S i))) u0 u x3
by (fsubst0_snd . . . . . previous)
fsubst0 (r (Bind Abst) (minus i0 (S i))) u0 d u d x3
end of h2
by (H2 . . . h1 . . h2)
we proved arity g d x3 (asucc g a0)
by (arity_abst . . . . . H23 . previous)
we proved arity g c2 (TLRef i) a0
(eq B Abst x0)→(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H17
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq B Abst x0
end of h2
by (h1 h2)
(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H16
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
case or4_intro2 : H11:ex3_4 B C C T λb:B.λe1:C.λ:C.λu1:T.eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λu1:T.getl i c2 (CHead e2 (Bind b) u1) λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H11 to prove arity g c2 (TLRef i) a0
case ex3_4_intro : x0:B x1:C x2:C x3:T H12:eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x3) H13:getl i c2 (CHead x2 (Bind x0) x3) H14:csubst0 (minus i0 (S i)) u0 x1 x2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H15)
by (minus_x_Sy . . H9)
we proved eq nat (minus i0 i) (S (minus i0 (S i)))
we proceed by induction on the previous result to prove
getl
S (minus i0 (S i))
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i0 i
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
consider H9
we proved lt i i0
that is equivalent to le (S i) i0
by (le_S . . previous)
we proved le (S i) (S i0)
by (le_S_n . . previous)
we proved le i i0
by (getl_conf_le . . . H3 . . H0 previous)
getl
minus i0 i
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
getl
S (minus i0 (S i))
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
end of H15
(H16)
by (f_equal . . . . . H12)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abst) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x3)
end of H16
(h1)
(H17)
by (f_equal . . . . . H12)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead d (Bind Abst) u
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead x1 (Bind x0) x3
end of H17
(h1)
(H18)
by (f_equal . . . . . H12)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d (Bind Abst) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead x1 (Bind x0) x3)
end of H18
suppose H19: eq B Abst x0
suppose H20: eq C d x1
(H21)
consider H18
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u x3
by (eq_ind_r . . . H13 . previous)
getl i c2 (CHead x2 (Bind x0) u)
end of H21
(H22)
by (eq_ind_r . . . H14 . H20)
csubst0 (minus i0 (S i)) u0 d x2
end of H22
(H23)
by (eq_ind_r . . . H21 . H19)
getl i c2 (CHead x2 (Bind Abst) u)
end of H23
(h1)
by (getl_gen_S . . . . . H15)
getl (r (Bind Abst) (minus i0 (S i))) d (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
consider H22
we proved csubst0 (minus i0 (S i)) u0 d x2
that is equivalent to csubst0 (r (Bind Abst) (minus i0 (S i))) u0 d x2
by (fsubst0_fst . . . . . previous)
fsubst0 (r (Bind Abst) (minus i0 (S i))) u0 d u x2 u
end of h2
by (H2 . . . h1 . . h2)
we proved arity g x2 u (asucc g a0)
by (arity_abst . . . . . H23 . previous)
we proved arity g c2 (TLRef i) a0
(eq B Abst x0)→(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H17
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq B Abst x0
end of h2
by (h1 h2)
(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H16
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
case or4_intro3 : H11:ex4_5 B C C T T λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λ:T.λw:T.getl i c2 (CHead e2 (Bind b) w) λ:B.λ:C.λ:C.λu1:T.λw:T.subst0 (minus i0 (S i)) u0 u1 w λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H11 to prove arity g c2 (TLRef i) a0
case ex4_5_intro : x0:B x1:C x2:C x3:T x4:T H12:eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x3) H13:getl i c2 (CHead x2 (Bind x0) x4) H14:subst0 (minus i0 (S i)) u0 x3 x4 H15:csubst0 (minus i0 (S i)) u0 x1 x2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H16)
by (minus_x_Sy . . H9)
we proved eq nat (minus i0 i) (S (minus i0 (S i)))
we proceed by induction on the previous result to prove
getl
S (minus i0 (S i))
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i0 i
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
consider H9
we proved lt i i0
that is equivalent to le (S i) i0
by (le_S . . previous)
we proved le (S i) (S i0)
by (le_S_n . . previous)
we proved le i i0
by (getl_conf_le . . . H3 . . H0 previous)
getl
minus i0 i
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
getl
S (minus i0 (S i))
CHead d (Bind Abst) u
CHead d1 (Bind Abbr) u0
end of H16
(H17)
by (f_equal . . . . . H12)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abst) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x3)
end of H17
(h1)
(H18)
by (f_equal . . . . . H12)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead d (Bind Abst) u
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead x1 (Bind x0) x3
end of H18
(h1)
(H19)
by (f_equal . . . . . H12)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d (Bind Abst) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead x1 (Bind x0) x3)
end of H19
suppose H20: eq B Abst x0
suppose H21: eq C d x1
(H22)
consider H19
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u x3
by (eq_ind_r . . . H14 . previous)
subst0 (minus i0 (S i)) u0 u x4
end of H22
(H23)
by (eq_ind_r . . . H15 . H21)
csubst0 (minus i0 (S i)) u0 d x2
end of H23
(H24)
by (eq_ind_r . . . H13 . H20)
getl i c2 (CHead x2 (Bind Abst) x4)
end of H24
(h1)
by (getl_gen_S . . . . . H16)
getl (r (Bind Abst) (minus i0 (S i))) d (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
(h1)
consider H22
we proved subst0 (minus i0 (S i)) u0 u x4
subst0 (r (Bind Abst) (minus i0 (S i))) u0 u x4
end of h1
(h2)
consider H23
we proved csubst0 (minus i0 (S i)) u0 d x2
csubst0 (r (Bind Abst) (minus i0 (S i))) u0 d x2
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (r (Bind Abst) (minus i0 (S i))) u0 d u x2 x4
end of h2
by (H2 . . . h1 . . h2)
we proved arity g x2 x4 (asucc g a0)
by (arity_abst . . . . . H24 . previous)
we proved arity g c2 (TLRef i) a0
(eq B Abst x0)→(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H18
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq B Abst x0
end of h2
by (h1 h2)
(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H17
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
we proved arity g c2 (TLRef i) a0
(lt i i0)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
suppose H9: le i0 i
by (csubst0_getl_ge . . H9 . . . H8 . H0)
we proved getl i c2 (CHead d (Bind Abst) u)
by (arity_abst . . . . . previous . H1)
we proved arity g c2 (TLRef i) a0
(le i0 i)→(arity g c2 (TLRef i) a0)
end of h2
by (lt_le_e . . . h1 h2)
arity g c2 (TLRef i) a0
arity g c2 t2 a0
arity g c2 t2 a0
case or3_intro2 : H6:land (subst0 i0 u0 (TLRef i) t2) (csubst0 i0 u0 c c2) ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H6 to prove arity g c2 t2 a0
case conj : H7:subst0 i0 u0 (TLRef i) t2 H8:csubst0 i0 u0 c c2 ⇒
the thesis becomes arity g c2 t2 a0
by (subst0_gen_lref . . . . H7)
we proved land (eq nat i i0) (eq T t2 (lift (S i) O u0))
we proceed by induction on the previous result to prove arity g c2 t2 a0
case conj : H9:eq nat i i0 H10:eq T t2 (lift (S i) O u0) ⇒
the thesis becomes arity g c2 t2 a0
(H12)
by (eq_ind_r . . . H3 . H9)
getl i c (CHead d1 (Bind Abbr) u0)
end of H12
(H14)
by (getl_mono . . . H0 . H12)
we proved eq C (CHead d (Bind Abst) u) (CHead d1 (Bind Abbr) u0)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead d1 (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead d1 (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H14
consider H14
we proved
<λ:C.Prop>
CASE CHead d1 (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove arity g c2 (lift (S i) O u0) a0
we proved arity g c2 (lift (S i) O u0) a0
by (eq_ind_r . . . previous . H10)
arity g c2 t2 a0
arity g c2 t2 a0
arity g c2 t2 a0
we proved arity g c2 t2 a0
∀d1:C
.∀u0:T.∀i0:nat.∀H3:(getl i0 c (CHead d1 (Bind Abbr) u0)).∀c2:C.∀t2:T.∀H4:(fsubst0 i0 u0 c (TLRef i) c2 t2).(arity g c2 t2 a0)
case arity_bind : b:B H0:not (eq B b Abst) c:C u:T a1:A H1:arity g c u a1 t:T a2:A :arity g (CHead c (Bind b) u) t a2 ⇒
the thesis becomes
∀d1:C
.∀u0:T
.∀i:nat
.∀H5:getl i c (CHead d1 (Bind Abbr) u0)
.∀c2:C.∀t2:T.∀H6:(fsubst0 i u0 c (THead (Bind b) u t) c2 t2).(arity g c2 t2 a2)
(H2) by induction hypothesis we know
∀d1:C
.∀u0:T
.∀i:nat
.(getl i c (CHead d1 (Bind Abbr) u0))→∀c2:C.∀t2:T.(fsubst0 i u0 c u c2 t2)→(arity g c2 t2 a1)
(H4) by induction hypothesis we know
∀d1:C
.∀u0:T
.∀i:nat
.getl i (CHead c (Bind b) u) (CHead d1 (Bind Abbr) u0)
→∀c2:C.∀t2:T.(fsubst0 i u0 (CHead c (Bind b) u) t c2 t2)→(arity g c2 t2 a2)
assume d1: C
assume u0: T
assume i: nat
suppose H5: getl i c (CHead d1 (Bind Abbr) u0)
assume c2: C
assume t2: T
suppose H6: fsubst0 i u0 c (THead (Bind b) u t) c2 t2
(H_x)
by (fsubst0_gen_base . . . . . . H6)
or3
land (eq C c c2) (subst0 i u0 (THead (Bind b) u t) t2)
land (eq T (THead (Bind b) u t) t2) (csubst0 i u0 c c2)
land (subst0 i u0 (THead (Bind b) u t) t2) (csubst0 i u0 c c2)
end of H_x
(H7) consider H_x
we proceed by induction on H7 to prove arity g c2 t2 a2
case or3_intro0 : H8:land (eq C c c2) (subst0 i u0 (THead (Bind b) u t) t2) ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H8 to prove arity g c2 t2 a2
case conj : H9:eq C c c2 H10:subst0 i u0 (THead (Bind b) u t) t2 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H9 to prove arity g c2 t2 a2
case refl_equal : ⇒
the thesis becomes arity g c t2 a2
by (subst0_gen_head . . . . . . H10)
we proved
or3
ex2 T λu2:T.eq T t2 (THead (Bind b) u2 t) λu2:T.subst0 i u0 u u2
ex2 T λt2:T.eq T t2 (THead (Bind b) u t2) λt2:T.subst0 (s (Bind b) i) u0 t t2
ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Bind b) u2 t2) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt2:T.subst0 (s (Bind b) i) u0 t t2
we proceed by induction on the previous result to prove arity g c t2 a2
case or3_intro0 : H11:ex2 T λu2:T.eq T t2 (THead (Bind b) u2 t) λu2:T.subst0 i u0 u u2 ⇒
the thesis becomes arity g c t2 a2
we proceed by induction on H11 to prove arity g c t2 a2
case ex_intro2 : x:T H12:eq T t2 (THead (Bind b) x t) H13:subst0 i u0 u x ⇒
the thesis becomes arity g c t2 a2
(h1)
by (fsubst0_snd . . . . . H13)
we proved fsubst0 i u0 c u c x
by (H2 . . . H5 . . previous)
arity g c x a1
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind b) u) (CHead c (Bind b) u)
by (getl_clear_bind . . . . previous . . H5)
getl (S i) (CHead c (Bind b) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
by (csubst0_snd_bind . . . . . H13 .)
we proved csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c (Bind b) x)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t (CHead c (Bind b) x) t
end of h2
by (H4 . . . h1 . . h2)
arity g (CHead c (Bind b) x) t a2
end of h2
by (arity_bind . . H0 . . . h1 . . h2)
we proved arity g c (THead (Bind b) x t) a2
by (eq_ind_r . . . previous . H12)
arity g c t2 a2
arity g c t2 a2
case or3_intro1 : H11:ex2 T λt3:T.eq T t2 (THead (Bind b) u t3) λt3:T.subst0 (s (Bind b) i) u0 t t3 ⇒
the thesis becomes arity g c t2 a2
we proceed by induction on H11 to prove arity g c t2 a2
case ex_intro2 : x:T H12:eq T t2 (THead (Bind b) u x) H13:subst0 (s (Bind b) i) u0 t x ⇒
the thesis becomes arity g c t2 a2
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind b) u) (CHead c (Bind b) u)
by (getl_clear_bind . . . . previous . . H5)
getl (S i) (CHead c (Bind b) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
consider H13
we proved subst0 (s (Bind b) i) u0 t x
that is equivalent to subst0 (S i) u0 t x
by (fsubst0_snd . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t (CHead c (Bind b) u) x
end of h2
by (H4 . . . h1 . . h2)
we proved arity g (CHead c (Bind b) u) x a2
by (arity_bind . . H0 . . . H1 . . previous)
we proved arity g c (THead (Bind b) u x) a2
by (eq_ind_r . . . previous . H12)
arity g c t2 a2
arity g c t2 a2
case or3_intro2 : H11:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Bind b) u2 t3) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt3:T.subst0 (s (Bind b) i) u0 t t3 ⇒
the thesis becomes arity g c t2 a2
we proceed by induction on H11 to prove arity g c t2 a2
case ex3_2_intro : x0:T x1:T H12:eq T t2 (THead (Bind b) x0 x1) H13:subst0 i u0 u x0 H14:subst0 (s (Bind b) i) u0 t x1 ⇒
the thesis becomes arity g c t2 a2
(h1)
by (fsubst0_snd . . . . . H13)
we proved fsubst0 i u0 c u c x0
by (H2 . . . H5 . . previous)
arity g c x0 a1
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind b) u) (CHead c (Bind b) u)
by (getl_clear_bind . . . . previous . . H5)
getl (S i) (CHead c (Bind b) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
(h1)
consider H14
we proved subst0 (s (Bind b) i) u0 t x1
subst0 (S i) u0 t x1
end of h1
(h2)
by (csubst0_snd_bind . . . . . H13 .)
csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c (Bind b) x0)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind b) u) t (CHead c (Bind b) x0) x1
end of h2
by (H4 . . . h1 . . h2)
arity g (CHead c (Bind b) x0) x1 a2
end of h2
by (arity_bind . . H0 . . . h1 . . h2)
we proved arity g c (THead (Bind b) x0 x1) a2
by (eq_ind_r . . . previous . H12)
arity g c t2 a2
arity g c t2 a2
arity g c t2 a2
arity g c2 t2 a2
arity g c2 t2 a2
case or3_intro1 : H8:land (eq T (THead (Bind b) u t) t2) (csubst0 i u0 c c2) ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H8 to prove arity g c2 t2 a2
case conj : H9:eq T (THead (Bind b) u t) t2 H10:csubst0 i u0 c c2 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H9 to prove arity g c2 t2 a2
case refl_equal : ⇒
the thesis becomes arity g c2 (THead (Bind b) u t) a2
(h1)
by (fsubst0_fst . . . . . H10)
we proved fsubst0 i u0 c u c2 u
by (H2 . . . H5 . . previous)
arity g c2 u a1
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind b) u) (CHead c (Bind b) u)
by (getl_clear_bind . . . . previous . . H5)
getl (S i) (CHead c (Bind b) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
by (csubst0_fst_bind . . . . . H10 .)
we proved csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c2 (Bind b) u)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t (CHead c2 (Bind b) u) t
end of h2
by (H4 . . . h1 . . h2)
arity g (CHead c2 (Bind b) u) t a2
end of h2
by (arity_bind . . H0 . . . h1 . . h2)
arity g c2 (THead (Bind b) u t) a2
arity g c2 t2 a2
arity g c2 t2 a2
case or3_intro2 : H8:land (subst0 i u0 (THead (Bind b) u t) t2) (csubst0 i u0 c c2) ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H8 to prove arity g c2 t2 a2
case conj : H9:subst0 i u0 (THead (Bind b) u t) t2 H10:csubst0 i u0 c c2 ⇒
the thesis becomes arity g c2 t2 a2
by (subst0_gen_head . . . . . . H9)
we proved
or3
ex2 T λu2:T.eq T t2 (THead (Bind b) u2 t) λu2:T.subst0 i u0 u u2
ex2 T λt2:T.eq T t2 (THead (Bind b) u t2) λt2:T.subst0 (s (Bind b) i) u0 t t2
ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Bind b) u2 t2) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt2:T.subst0 (s (Bind b) i) u0 t t2
we proceed by induction on the previous result to prove arity g c2 t2 a2
case or3_intro0 : H11:ex2 T λu2:T.eq T t2 (THead (Bind b) u2 t) λu2:T.subst0 i u0 u u2 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H11 to prove arity g c2 t2 a2
case ex_intro2 : x:T H12:eq T t2 (THead (Bind b) x t) H13:subst0 i u0 u x ⇒
the thesis becomes arity g c2 t2 a2
(h1)
by (fsubst0_both . . . . . H13 . H10)
we proved fsubst0 i u0 c u c2 x
by (H2 . . . H5 . . previous)
arity g c2 x a1
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind b) u) (CHead c (Bind b) u)
by (getl_clear_bind . . . . previous . . H5)
getl (S i) (CHead c (Bind b) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
by (csubst0_both_bind . . . . . H13 . . H10)
we proved csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c2 (Bind b) x)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t (CHead c2 (Bind b) x) t
end of h2
by (H4 . . . h1 . . h2)
arity g (CHead c2 (Bind b) x) t a2
end of h2
by (arity_bind . . H0 . . . h1 . . h2)
we proved arity g c2 (THead (Bind b) x t) a2
by (eq_ind_r . . . previous . H12)
arity g c2 t2 a2
arity g c2 t2 a2
case or3_intro1 : H11:ex2 T λt3:T.eq T t2 (THead (Bind b) u t3) λt3:T.subst0 (s (Bind b) i) u0 t t3 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H11 to prove arity g c2 t2 a2
case ex_intro2 : x:T H12:eq T t2 (THead (Bind b) u x) H13:subst0 (s (Bind b) i) u0 t x ⇒
the thesis becomes arity g c2 t2 a2
(h1)
by (fsubst0_fst . . . . . H10)
we proved fsubst0 i u0 c u c2 u
by (H2 . . . H5 . . previous)
arity g c2 u a1
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind b) u) (CHead c (Bind b) u)
by (getl_clear_bind . . . . previous . . H5)
getl (S i) (CHead c (Bind b) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
(h1)
consider H13
we proved subst0 (s (Bind b) i) u0 t x
subst0 (S i) u0 t x
end of h1
(h2)
by (csubst0_fst_bind . . . . . H10 .)
csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c2 (Bind b) u)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind b) u) t (CHead c2 (Bind b) u) x
end of h2
by (H4 . . . h1 . . h2)
arity g (CHead c2 (Bind b) u) x a2
end of h2
by (arity_bind . . H0 . . . h1 . . h2)
we proved arity g c2 (THead (Bind b) u x) a2
by (eq_ind_r . . . previous . H12)
arity g c2 t2 a2
arity g c2 t2 a2
case or3_intro2 : H11:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Bind b) u2 t3) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt3:T.subst0 (s (Bind b) i) u0 t t3 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H11 to prove arity g c2 t2 a2
case ex3_2_intro : x0:T x1:T H12:eq T t2 (THead (Bind b) x0 x1) H13:subst0 i u0 u x0 H14:subst0 (s (Bind b) i) u0 t x1 ⇒
the thesis becomes arity g c2 t2 a2
(h1)
by (fsubst0_both . . . . . H13 . H10)
we proved fsubst0 i u0 c u c2 x0
by (H2 . . . H5 . . previous)
arity g c2 x0 a1
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind b) u) (CHead c (Bind b) u)
by (getl_clear_bind . . . . previous . . H5)
getl (S i) (CHead c (Bind b) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
(h1)
consider H14
we proved subst0 (s (Bind b) i) u0 t x1
subst0 (S i) u0 t x1
end of h1
(h2)
by (csubst0_both_bind . . . . . H13 . . H10)
csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c2 (Bind b) x0)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind b) u) t (CHead c2 (Bind b) x0) x1
end of h2
by (H4 . . . h1 . . h2)
arity g (CHead c2 (Bind b) x0) x1 a2
end of h2
by (arity_bind . . H0 . . . h1 . . h2)
we proved arity g c2 (THead (Bind b) x0 x1) a2
by (eq_ind_r . . . previous . H12)
arity g c2 t2 a2
arity g c2 t2 a2
arity g c2 t2 a2
arity g c2 t2 a2
we proved arity g c2 t2 a2
∀d1:C
.∀u0:T
.∀i:nat
.∀H5:getl i c (CHead d1 (Bind Abbr) u0)
.∀c2:C.∀t2:T.∀H6:(fsubst0 i u0 c (THead (Bind b) u t) c2 t2).(arity g c2 t2 a2)
case arity_head : c:C u:T a1:A H0:arity g c u (asucc g a1) t:T a2:A :arity g (CHead c (Bind Abst) u) t a2 ⇒
the thesis becomes
∀d1:C
.∀u0:T
.∀i:nat
.∀H4:getl i c (CHead d1 (Bind Abbr) u0)
.∀c2:C.∀t2:T.∀H5:(fsubst0 i u0 c (THead (Bind Abst) u t) c2 t2).(arity g c2 t2 (AHead a1 a2))
(H1) by induction hypothesis we know
∀d1:C
.∀u0:T
.∀i:nat
.getl i c (CHead d1 (Bind Abbr) u0)
→∀c2:C.∀t2:T.(fsubst0 i u0 c u c2 t2)→(arity g c2 t2 (asucc g a1))
(H3) by induction hypothesis we know
∀d1:C
.∀u0:T
.∀i:nat
.getl i (CHead c (Bind Abst) u) (CHead d1 (Bind Abbr) u0)
→∀c2:C.∀t2:T.(fsubst0 i u0 (CHead c (Bind Abst) u) t c2 t2)→(arity g c2 t2 a2)
assume d1: C
assume u0: T
assume i: nat
suppose H4: getl i c (CHead d1 (Bind Abbr) u0)
assume c2: C
assume t2: T
suppose H5: fsubst0 i u0 c (THead (Bind Abst) u t) c2 t2
(H_x)
by (fsubst0_gen_base . . . . . . H5)
or3
land (eq C c c2) (subst0 i u0 (THead (Bind Abst) u t) t2)
land (eq T (THead (Bind Abst) u t) t2) (csubst0 i u0 c c2)
land (subst0 i u0 (THead (Bind Abst) u t) t2) (csubst0 i u0 c c2)
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove arity g c2 t2 (AHead a1 a2)
case or3_intro0 : H7:land (eq C c c2) (subst0 i u0 (THead (Bind Abst) u t) t2) ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
we proceed by induction on H7 to prove arity g c2 t2 (AHead a1 a2)
case conj : H8:eq C c c2 H9:subst0 i u0 (THead (Bind Abst) u t) t2 ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
we proceed by induction on H8 to prove arity g c2 t2 (AHead a1 a2)
case refl_equal : ⇒
the thesis becomes arity g c t2 (AHead a1 a2)
by (subst0_gen_head . . . . . . H9)
we proved
or3
ex2 T λu2:T.eq T t2 (THead (Bind Abst) u2 t) λu2:T.subst0 i u0 u u2
ex2 T λt2:T.eq T t2 (THead (Bind Abst) u t2) λt2:T.subst0 (s (Bind Abst) i) u0 t t2
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Bind Abst) u2 t2)
λu2:T.λ:T.subst0 i u0 u u2
λ:T.λt2:T.subst0 (s (Bind Abst) i) u0 t t2
we proceed by induction on the previous result to prove arity g c t2 (AHead a1 a2)
case or3_intro0 : H10:ex2 T λu2:T.eq T t2 (THead (Bind Abst) u2 t) λu2:T.subst0 i u0 u u2 ⇒
the thesis becomes arity g c t2 (AHead a1 a2)
we proceed by induction on H10 to prove arity g c t2 (AHead a1 a2)
case ex_intro2 : x:T H11:eq T t2 (THead (Bind Abst) x t) H12:subst0 i u0 u x ⇒
the thesis becomes arity g c t2 (AHead a1 a2)
(h1)
by (fsubst0_snd . . . . . H12)
we proved fsubst0 i u0 c u c x
by (H1 . . . H4 . . previous)
arity g c x (asucc g a1)
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind Abst) u) (CHead c (Bind Abst) u)
by (getl_clear_bind . . . . previous . . H4)
getl (S i) (CHead c (Bind Abst) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
by (csubst0_snd_bind . . . . . H12 .)
we proved csubst0 (S i) u0 (CHead c (Bind Abst) u) (CHead c (Bind Abst) x)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind Abst) u) t (CHead c (Bind Abst) x) t
end of h2
by (H3 . . . h1 . . h2)
arity g (CHead c (Bind Abst) x) t a2
end of h2
by (arity_head . . . . h1 . . h2)
we proved arity g c (THead (Bind Abst) x t) (AHead a1 a2)
by (eq_ind_r . . . previous . H11)
arity g c t2 (AHead a1 a2)
arity g c t2 (AHead a1 a2)
case or3_intro1 : H10:ex2 T λt3:T.eq T t2 (THead (Bind Abst) u t3) λt3:T.subst0 (s (Bind Abst) i) u0 t t3 ⇒
the thesis becomes arity g c t2 (AHead a1 a2)
we proceed by induction on H10 to prove arity g c t2 (AHead a1 a2)
case ex_intro2 : x:T H11:eq T t2 (THead (Bind Abst) u x) H12:subst0 (s (Bind Abst) i) u0 t x ⇒
the thesis becomes arity g c t2 (AHead a1 a2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind Abst) u) (CHead c (Bind Abst) u)
by (getl_clear_bind . . . . previous . . H4)
getl (S i) (CHead c (Bind Abst) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
consider H12
we proved subst0 (s (Bind Abst) i) u0 t x
that is equivalent to subst0 (S i) u0 t x
by (fsubst0_snd . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind Abst) u) t (CHead c (Bind Abst) u) x
end of h2
by (H3 . . . h1 . . h2)
we proved arity g (CHead c (Bind Abst) u) x a2
by (arity_head . . . . H0 . . previous)
we proved arity g c (THead (Bind Abst) u x) (AHead a1 a2)
by (eq_ind_r . . . previous . H11)
arity g c t2 (AHead a1 a2)
arity g c t2 (AHead a1 a2)
case or3_intro2 : H10:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Bind Abst) u2 t3) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt3:T.subst0 (s (Bind Abst) i) u0 t t3 ⇒
the thesis becomes arity g c t2 (AHead a1 a2)
we proceed by induction on H10 to prove arity g c t2 (AHead a1 a2)
case ex3_2_intro : x0:T x1:T H11:eq T t2 (THead (Bind Abst) x0 x1) H12:subst0 i u0 u x0 H13:subst0 (s (Bind Abst) i) u0 t x1 ⇒
the thesis becomes arity g c t2 (AHead a1 a2)
(h1)
by (fsubst0_snd . . . . . H12)
we proved fsubst0 i u0 c u c x0
by (H1 . . . H4 . . previous)
arity g c x0 (asucc g a1)
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind Abst) u) (CHead c (Bind Abst) u)
by (getl_clear_bind . . . . previous . . H4)
getl (S i) (CHead c (Bind Abst) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
(h1)
consider H13
we proved subst0 (s (Bind Abst) i) u0 t x1
subst0 (S i) u0 t x1
end of h1
(h2)
by (csubst0_snd_bind . . . . . H12 .)
csubst0 (S i) u0 (CHead c (Bind Abst) u) (CHead c (Bind Abst) x0)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind Abst) u) t (CHead c (Bind Abst) x0) x1
end of h2
by (H3 . . . h1 . . h2)
arity g (CHead c (Bind Abst) x0) x1 a2
end of h2
by (arity_head . . . . h1 . . h2)
we proved arity g c (THead (Bind Abst) x0 x1) (AHead a1 a2)
by (eq_ind_r . . . previous . H11)
arity g c t2 (AHead a1 a2)
arity g c t2 (AHead a1 a2)
arity g c t2 (AHead a1 a2)
arity g c2 t2 (AHead a1 a2)
arity g c2 t2 (AHead a1 a2)
case or3_intro1 : H7:land (eq T (THead (Bind Abst) u t) t2) (csubst0 i u0 c c2) ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
we proceed by induction on H7 to prove arity g c2 t2 (AHead a1 a2)
case conj : H8:eq T (THead (Bind Abst) u t) t2 H9:csubst0 i u0 c c2 ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
we proceed by induction on H8 to prove arity g c2 t2 (AHead a1 a2)
case refl_equal : ⇒
the thesis becomes arity g c2 (THead (Bind Abst) u t) (AHead a1 a2)
(h1)
by (fsubst0_fst . . . . . H9)
we proved fsubst0 i u0 c u c2 u
by (H1 . . . H4 . . previous)
arity g c2 u (asucc g a1)
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind Abst) u) (CHead c (Bind Abst) u)
by (getl_clear_bind . . . . previous . . H4)
getl (S i) (CHead c (Bind Abst) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
by (csubst0_fst_bind . . . . . H9 .)
we proved csubst0 (S i) u0 (CHead c (Bind Abst) u) (CHead c2 (Bind Abst) u)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind Abst) u) t (CHead c2 (Bind Abst) u) t
end of h2
by (H3 . . . h1 . . h2)
arity g (CHead c2 (Bind Abst) u) t a2
end of h2
by (arity_head . . . . h1 . . h2)
arity g c2 (THead (Bind Abst) u t) (AHead a1 a2)
arity g c2 t2 (AHead a1 a2)
arity g c2 t2 (AHead a1 a2)
case or3_intro2 : H7:land (subst0 i u0 (THead (Bind Abst) u t) t2) (csubst0 i u0 c c2) ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
we proceed by induction on H7 to prove arity g c2 t2 (AHead a1 a2)
case conj : H8:subst0 i u0 (THead (Bind Abst) u t) t2 H9:csubst0 i u0 c c2 ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
by (subst0_gen_head . . . . . . H8)
we proved
or3
ex2 T λu2:T.eq T t2 (THead (Bind Abst) u2 t) λu2:T.subst0 i u0 u u2
ex2 T λt2:T.eq T t2 (THead (Bind Abst) u t2) λt2:T.subst0 (s (Bind Abst) i) u0 t t2
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Bind Abst) u2 t2)
λu2:T.λ:T.subst0 i u0 u u2
λ:T.λt2:T.subst0 (s (Bind Abst) i) u0 t t2
we proceed by induction on the previous result to prove arity g c2 t2 (AHead a1 a2)
case or3_intro0 : H10:ex2 T λu2:T.eq T t2 (THead (Bind Abst) u2 t) λu2:T.subst0 i u0 u u2 ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
we proceed by induction on H10 to prove arity g c2 t2 (AHead a1 a2)
case ex_intro2 : x:T H11:eq T t2 (THead (Bind Abst) x t) H12:subst0 i u0 u x ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
(h1)
by (fsubst0_both . . . . . H12 . H9)
we proved fsubst0 i u0 c u c2 x
by (H1 . . . H4 . . previous)
arity g c2 x (asucc g a1)
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind Abst) u) (CHead c (Bind Abst) u)
by (getl_clear_bind . . . . previous . . H4)
getl (S i) (CHead c (Bind Abst) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
by (csubst0_both_bind . . . . . H12 . . H9)
we proved csubst0 (S i) u0 (CHead c (Bind Abst) u) (CHead c2 (Bind Abst) x)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind Abst) u) t (CHead c2 (Bind Abst) x) t
end of h2
by (H3 . . . h1 . . h2)
arity g (CHead c2 (Bind Abst) x) t a2
end of h2
by (arity_head . . . . h1 . . h2)
we proved arity g c2 (THead (Bind Abst) x t) (AHead a1 a2)
by (eq_ind_r . . . previous . H11)
arity g c2 t2 (AHead a1 a2)
arity g c2 t2 (AHead a1 a2)
case or3_intro1 : H10:ex2 T λt3:T.eq T t2 (THead (Bind Abst) u t3) λt3:T.subst0 (s (Bind Abst) i) u0 t t3 ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
we proceed by induction on H10 to prove arity g c2 t2 (AHead a1 a2)
case ex_intro2 : x:T H11:eq T t2 (THead (Bind Abst) u x) H12:subst0 (s (Bind Abst) i) u0 t x ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
(h1)
by (fsubst0_fst . . . . . H9)
we proved fsubst0 i u0 c u c2 u
by (H1 . . . H4 . . previous)
arity g c2 u (asucc g a1)
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind Abst) u) (CHead c (Bind Abst) u)
by (getl_clear_bind . . . . previous . . H4)
getl (S i) (CHead c (Bind Abst) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
(h1)
consider H12
we proved subst0 (s (Bind Abst) i) u0 t x
subst0 (S i) u0 t x
end of h1
(h2)
by (csubst0_fst_bind . . . . . H9 .)
csubst0 (S i) u0 (CHead c (Bind Abst) u) (CHead c2 (Bind Abst) u)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind Abst) u) t (CHead c2 (Bind Abst) u) x
end of h2
by (H3 . . . h1 . . h2)
arity g (CHead c2 (Bind Abst) u) x a2
end of h2
by (arity_head . . . . h1 . . h2)
we proved arity g c2 (THead (Bind Abst) u x) (AHead a1 a2)
by (eq_ind_r . . . previous . H11)
arity g c2 t2 (AHead a1 a2)
arity g c2 t2 (AHead a1 a2)
case or3_intro2 : H10:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Bind Abst) u2 t3) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt3:T.subst0 (s (Bind Abst) i) u0 t t3 ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
we proceed by induction on H10 to prove arity g c2 t2 (AHead a1 a2)
case ex3_2_intro : x0:T x1:T H11:eq T t2 (THead (Bind Abst) x0 x1) H12:subst0 i u0 u x0 H13:subst0 (s (Bind Abst) i) u0 t x1 ⇒
the thesis becomes arity g c2 t2 (AHead a1 a2)
(h1)
by (fsubst0_both . . . . . H12 . H9)
we proved fsubst0 i u0 c u c2 x0
by (H1 . . . H4 . . previous)
arity g c2 x0 (asucc g a1)
end of h1
(h2)
(h1)
by (clear_bind . . .)
we proved clear (CHead c (Bind Abst) u) (CHead c (Bind Abst) u)
by (getl_clear_bind . . . . previous . . H4)
getl (S i) (CHead c (Bind Abst) u) (CHead d1 (Bind Abbr) u0)
end of h1
(h2)
(h1)
consider H13
we proved subst0 (s (Bind Abst) i) u0 t x1
subst0 (S i) u0 t x1
end of h1
(h2)
by (csubst0_both_bind . . . . . H12 . . H9)
csubst0 (S i) u0 (CHead c (Bind Abst) u) (CHead c2 (Bind Abst) x0)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind Abst) u) t (CHead c2 (Bind Abst) x0) x1
end of h2
by (H3 . . . h1 . . h2)
arity g (CHead c2 (Bind Abst) x0) x1 a2
end of h2
by (arity_head . . . . h1 . . h2)
we proved arity g c2 (THead (Bind Abst) x0 x1) (AHead a1 a2)
by (eq_ind_r . . . previous . H11)
arity g c2 t2 (AHead a1 a2)
arity g c2 t2 (AHead a1 a2)
arity g c2 t2 (AHead a1 a2)
arity g c2 t2 (AHead a1 a2)
we proved arity g c2 t2 (AHead a1 a2)
∀d1:C
.∀u0:T
.∀i:nat
.∀H4:getl i c (CHead d1 (Bind Abbr) u0)
.∀c2:C.∀t2:T.∀H5:(fsubst0 i u0 c (THead (Bind Abst) u t) c2 t2).(arity g c2 t2 (AHead a1 a2))
case arity_appl : c:C u:T a1:A H0:arity g c u a1 t:T a2:A H2:arity g c t (AHead a1 a2) ⇒
the thesis becomes
∀d1:C
.∀u0:T
.∀i:nat
.∀H4:getl i c (CHead d1 (Bind Abbr) u0)
.∀c2:C.∀t2:T.∀H5:(fsubst0 i u0 c (THead (Flat Appl) u t) c2 t2).(arity g c2 t2 a2)
(H1) by induction hypothesis we know
∀d1:C
.∀u0:T
.∀i:nat
.(getl i c (CHead d1 (Bind Abbr) u0))→∀c2:C.∀t2:T.(fsubst0 i u0 c u c2 t2)→(arity g c2 t2 a1)
(H3) by induction hypothesis we know
∀d1:C
.∀u0:T
.∀i:nat
.getl i c (CHead d1 (Bind Abbr) u0)
→∀c2:C.∀t2:T.(fsubst0 i u0 c t c2 t2)→(arity g c2 t2 (AHead a1 a2))
assume d1: C
assume u0: T
assume i: nat
suppose H4: getl i c (CHead d1 (Bind Abbr) u0)
assume c2: C
assume t2: T
suppose H5: fsubst0 i u0 c (THead (Flat Appl) u t) c2 t2
(H_x)
by (fsubst0_gen_base . . . . . . H5)
or3
land (eq C c c2) (subst0 i u0 (THead (Flat Appl) u t) t2)
land (eq T (THead (Flat Appl) u t) t2) (csubst0 i u0 c c2)
land (subst0 i u0 (THead (Flat Appl) u t) t2) (csubst0 i u0 c c2)
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove arity g c2 t2 a2
case or3_intro0 : H7:land (eq C c c2) (subst0 i u0 (THead (Flat Appl) u t) t2) ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H7 to prove arity g c2 t2 a2
case conj : H8:eq C c c2 H9:subst0 i u0 (THead (Flat Appl) u t) t2 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H8 to prove arity g c2 t2 a2
case refl_equal : ⇒
the thesis becomes arity g c t2 a2
by (subst0_gen_head . . . . . . H9)
we proved
or3
ex2 T λu2:T.eq T t2 (THead (Flat Appl) u2 t) λu2:T.subst0 i u0 u u2
ex2 T λt2:T.eq T t2 (THead (Flat Appl) u t2) λt2:T.subst0 (s (Flat Appl) i) u0 t t2
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.subst0 i u0 u u2
λ:T.λt2:T.subst0 (s (Flat Appl) i) u0 t t2
we proceed by induction on the previous result to prove arity g c t2 a2
case or3_intro0 : H10:ex2 T λu2:T.eq T t2 (THead (Flat Appl) u2 t) λu2:T.subst0 i u0 u u2 ⇒
the thesis becomes arity g c t2 a2
we proceed by induction on H10 to prove arity g c t2 a2
case ex_intro2 : x:T H11:eq T t2 (THead (Flat Appl) x t) H12:subst0 i u0 u x ⇒
the thesis becomes arity g c t2 a2
by (fsubst0_snd . . . . . H12)
we proved fsubst0 i u0 c u c x
by (H1 . . . H4 . . previous)
we proved arity g c x a1
by (arity_appl . . . . previous . . H2)
we proved arity g c (THead (Flat Appl) x t) a2
by (eq_ind_r . . . previous . H11)
arity g c t2 a2
arity g c t2 a2
case or3_intro1 : H10:ex2 T λt3:T.eq T t2 (THead (Flat Appl) u t3) λt3:T.subst0 (s (Flat Appl) i) u0 t t3 ⇒
the thesis becomes arity g c t2 a2
we proceed by induction on H10 to prove arity g c t2 a2
case ex_intro2 : x:T H11:eq T t2 (THead (Flat Appl) u x) H12:subst0 (s (Flat Appl) i) u0 t x ⇒
the thesis becomes arity g c t2 a2
consider H12
we proved subst0 (s (Flat Appl) i) u0 t x
that is equivalent to subst0 i u0 t x
by (fsubst0_snd . . . . . previous)
we proved fsubst0 i u0 c t c x
by (H3 . . . H4 . . previous)
we proved arity g c x (AHead a1 a2)
by (arity_appl . . . . H0 . . previous)
we proved arity g c (THead (Flat Appl) u x) a2
by (eq_ind_r . . . previous . H11)
arity g c t2 a2
arity g c t2 a2
case or3_intro2 : H10:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt3:T.subst0 (s (Flat Appl) i) u0 t t3 ⇒
the thesis becomes arity g c t2 a2
we proceed by induction on H10 to prove arity g c t2 a2
case ex3_2_intro : x0:T x1:T H11:eq T t2 (THead (Flat Appl) x0 x1) H12:subst0 i u0 u x0 H13:subst0 (s (Flat Appl) i) u0 t x1 ⇒
the thesis becomes arity g c t2 a2
(h1)
by (fsubst0_snd . . . . . H12)
we proved fsubst0 i u0 c u c x0
by (H1 . . . H4 . . previous)
arity g c x0 a1
end of h1
(h2)
consider H13
we proved subst0 (s (Flat Appl) i) u0 t x1
that is equivalent to subst0 i u0 t x1
by (fsubst0_snd . . . . . previous)
we proved fsubst0 i u0 c t c x1
by (H3 . . . H4 . . previous)
arity g c x1 (AHead a1 a2)
end of h2
by (arity_appl . . . . h1 . . h2)
we proved arity g c (THead (Flat Appl) x0 x1) a2
by (eq_ind_r . . . previous . H11)
arity g c t2 a2
arity g c t2 a2
arity g c t2 a2
arity g c2 t2 a2
arity g c2 t2 a2
case or3_intro1 : H7:land (eq T (THead (Flat Appl) u t) t2) (csubst0 i u0 c c2) ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H7 to prove arity g c2 t2 a2
case conj : H8:eq T (THead (Flat Appl) u t) t2 H9:csubst0 i u0 c c2 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H8 to prove arity g c2 t2 a2
case refl_equal : ⇒
the thesis becomes arity g c2 (THead (Flat Appl) u t) a2
(h1)
by (fsubst0_fst . . . . . H9)
we proved fsubst0 i u0 c u c2 u
by (H1 . . . H4 . . previous)
arity g c2 u a1
end of h1
(h2)
by (fsubst0_fst . . . . . H9)
we proved fsubst0 i u0 c t c2 t
by (H3 . . . H4 . . previous)
arity g c2 t (AHead a1 a2)
end of h2
by (arity_appl . . . . h1 . . h2)
arity g c2 (THead (Flat Appl) u t) a2
arity g c2 t2 a2
arity g c2 t2 a2
case or3_intro2 : H7:land (subst0 i u0 (THead (Flat Appl) u t) t2) (csubst0 i u0 c c2) ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H7 to prove arity g c2 t2 a2
case conj : H8:subst0 i u0 (THead (Flat Appl) u t) t2 H9:csubst0 i u0 c c2 ⇒
the thesis becomes arity g c2 t2 a2
by (subst0_gen_head . . . . . . H8)
we proved
or3
ex2 T λu2:T.eq T t2 (THead (Flat Appl) u2 t) λu2:T.subst0 i u0 u u2
ex2 T λt2:T.eq T t2 (THead (Flat Appl) u t2) λt2:T.subst0 (s (Flat Appl) i) u0 t t2
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.subst0 i u0 u u2
λ:T.λt2:T.subst0 (s (Flat Appl) i) u0 t t2
we proceed by induction on the previous result to prove arity g c2 t2 a2
case or3_intro0 : H10:ex2 T λu2:T.eq T t2 (THead (Flat Appl) u2 t) λu2:T.subst0 i u0 u u2 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H10 to prove arity g c2 t2 a2
case ex_intro2 : x:T H11:eq T t2 (THead (Flat Appl) x t) H12:subst0 i u0 u x ⇒
the thesis becomes arity g c2 t2 a2
(h1)
by (fsubst0_both . . . . . H12 . H9)
we proved fsubst0 i u0 c u c2 x
by (H1 . . . H4 . . previous)
arity g c2 x a1
end of h1
(h2)
by (fsubst0_fst . . . . . H9)
we proved fsubst0 i u0 c t c2 t
by (H3 . . . H4 . . previous)
arity g c2 t (AHead a1 a2)
end of h2
by (arity_appl . . . . h1 . . h2)
we proved arity g c2 (THead (Flat Appl) x t) a2
by (eq_ind_r . . . previous . H11)
arity g c2 t2 a2
arity g c2 t2 a2
case or3_intro1 : H10:ex2 T λt3:T.eq T t2 (THead (Flat Appl) u t3) λt3:T.subst0 (s (Flat Appl) i) u0 t t3 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H10 to prove arity g c2 t2 a2
case ex_intro2 : x:T H11:eq T t2 (THead (Flat Appl) u x) H12:subst0 (s (Flat Appl) i) u0 t x ⇒
the thesis becomes arity g c2 t2 a2
(h1)
by (fsubst0_fst . . . . . H9)
we proved fsubst0 i u0 c u c2 u
by (H1 . . . H4 . . previous)
arity g c2 u a1
end of h1
(h2)
consider H12
we proved subst0 (s (Flat Appl) i) u0 t x
that is equivalent to subst0 i u0 t x
by (fsubst0_both . . . . . previous . H9)
we proved fsubst0 i u0 c t c2 x
by (H3 . . . H4 . . previous)
arity g c2 x (AHead a1 a2)
end of h2
by (arity_appl . . . . h1 . . h2)
we proved arity g c2 (THead (Flat Appl) u x) a2
by (eq_ind_r . . . previous . H11)
arity g c2 t2 a2
arity g c2 t2 a2
case or3_intro2 : H10:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt3:T.subst0 (s (Flat Appl) i) u0 t t3 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H10 to prove arity g c2 t2 a2
case ex3_2_intro : x0:T x1:T H11:eq T t2 (THead (Flat Appl) x0 x1) H12:subst0 i u0 u x0 H13:subst0 (s (Flat Appl) i) u0 t x1 ⇒
the thesis becomes arity g c2 t2 a2
(h1)
by (fsubst0_both . . . . . H12 . H9)
we proved fsubst0 i u0 c u c2 x0
by (H1 . . . H4 . . previous)
arity g c2 x0 a1
end of h1
(h2)
consider H13
we proved subst0 (s (Flat Appl) i) u0 t x1
that is equivalent to subst0 i u0 t x1
by (fsubst0_both . . . . . previous . H9)
we proved fsubst0 i u0 c t c2 x1
by (H3 . . . H4 . . previous)
arity g c2 x1 (AHead a1 a2)
end of h2
by (arity_appl . . . . h1 . . h2)
we proved arity g c2 (THead (Flat Appl) x0 x1) a2
by (eq_ind_r . . . previous . H11)
arity g c2 t2 a2
arity g c2 t2 a2
arity g c2 t2 a2
arity g c2 t2 a2
we proved arity g c2 t2 a2
∀d1:C
.∀u0:T
.∀i:nat
.∀H4:getl i c (CHead d1 (Bind Abbr) u0)
.∀c2:C.∀t2:T.∀H5:(fsubst0 i u0 c (THead (Flat Appl) u t) c2 t2).(arity g c2 t2 a2)
case arity_cast : c:C u:T a0:A H0:arity g c u (asucc g a0) t:T H2:arity g c t a0 ⇒
the thesis becomes
∀d1:C
.∀u0:T
.∀i:nat
.∀H4:getl i c (CHead d1 (Bind Abbr) u0)
.∀c2:C.∀t2:T.∀H5:(fsubst0 i u0 c (THead (Flat Cast) u t) c2 t2).(arity g c2 t2 a0)
(H1) by induction hypothesis we know
∀d1:C
.∀u0:T
.∀i:nat
.getl i c (CHead d1 (Bind Abbr) u0)
→∀c2:C.∀t2:T.(fsubst0 i u0 c u c2 t2)→(arity g c2 t2 (asucc g a0))
(H3) by induction hypothesis we know
∀d1:C
.∀u0:T
.∀i:nat
.(getl i c (CHead d1 (Bind Abbr) u0))→∀c2:C.∀t2:T.(fsubst0 i u0 c t c2 t2)→(arity g c2 t2 a0)
assume d1: C
assume u0: T
assume i: nat
suppose H4: getl i c (CHead d1 (Bind Abbr) u0)
assume c2: C
assume t2: T
suppose H5: fsubst0 i u0 c (THead (Flat Cast) u t) c2 t2
(H_x)
by (fsubst0_gen_base . . . . . . H5)
or3
land (eq C c c2) (subst0 i u0 (THead (Flat Cast) u t) t2)
land (eq T (THead (Flat Cast) u t) t2) (csubst0 i u0 c c2)
land (subst0 i u0 (THead (Flat Cast) u t) t2) (csubst0 i u0 c c2)
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove arity g c2 t2 a0
case or3_intro0 : H7:land (eq C c c2) (subst0 i u0 (THead (Flat Cast) u t) t2) ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H7 to prove arity g c2 t2 a0
case conj : H8:eq C c c2 H9:subst0 i u0 (THead (Flat Cast) u t) t2 ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H8 to prove arity g c2 t2 a0
case refl_equal : ⇒
the thesis becomes arity g c t2 a0
by (subst0_gen_head . . . . . . H9)
we proved
or3
ex2 T λu2:T.eq T t2 (THead (Flat Cast) u2 t) λu2:T.subst0 i u0 u u2
ex2 T λt2:T.eq T t2 (THead (Flat Cast) u t2) λt2:T.subst0 (s (Flat Cast) i) u0 t t2
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Flat Cast) u2 t2)
λu2:T.λ:T.subst0 i u0 u u2
λ:T.λt2:T.subst0 (s (Flat Cast) i) u0 t t2
we proceed by induction on the previous result to prove arity g c t2 a0
case or3_intro0 : H10:ex2 T λu2:T.eq T t2 (THead (Flat Cast) u2 t) λu2:T.subst0 i u0 u u2 ⇒
the thesis becomes arity g c t2 a0
we proceed by induction on H10 to prove arity g c t2 a0
case ex_intro2 : x:T H11:eq T t2 (THead (Flat Cast) x t) H12:subst0 i u0 u x ⇒
the thesis becomes arity g c t2 a0
by (fsubst0_snd . . . . . H12)
we proved fsubst0 i u0 c u c x
by (H1 . . . H4 . . previous)
we proved arity g c x (asucc g a0)
by (arity_cast . . . . previous . H2)
we proved arity g c (THead (Flat Cast) x t) a0
by (eq_ind_r . . . previous . H11)
arity g c t2 a0
arity g c t2 a0
case or3_intro1 : H10:ex2 T λt3:T.eq T t2 (THead (Flat Cast) u t3) λt3:T.subst0 (s (Flat Cast) i) u0 t t3 ⇒
the thesis becomes arity g c t2 a0
we proceed by induction on H10 to prove arity g c t2 a0
case ex_intro2 : x:T H11:eq T t2 (THead (Flat Cast) u x) H12:subst0 (s (Flat Cast) i) u0 t x ⇒
the thesis becomes arity g c t2 a0
consider H12
we proved subst0 (s (Flat Cast) i) u0 t x
that is equivalent to subst0 i u0 t x
by (fsubst0_snd . . . . . previous)
we proved fsubst0 i u0 c t c x
by (H3 . . . H4 . . previous)
we proved arity g c x a0
by (arity_cast . . . . H0 . previous)
we proved arity g c (THead (Flat Cast) u x) a0
by (eq_ind_r . . . previous . H11)
arity g c t2 a0
arity g c t2 a0
case or3_intro2 : H10:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt3:T.subst0 (s (Flat Cast) i) u0 t t3 ⇒
the thesis becomes arity g c t2 a0
we proceed by induction on H10 to prove arity g c t2 a0
case ex3_2_intro : x0:T x1:T H11:eq T t2 (THead (Flat Cast) x0 x1) H12:subst0 i u0 u x0 H13:subst0 (s (Flat Cast) i) u0 t x1 ⇒
the thesis becomes arity g c t2 a0
(h1)
by (fsubst0_snd . . . . . H12)
we proved fsubst0 i u0 c u c x0
by (H1 . . . H4 . . previous)
arity g c x0 (asucc g a0)
end of h1
(h2)
consider H13
we proved subst0 (s (Flat Cast) i) u0 t x1
that is equivalent to subst0 i u0 t x1
by (fsubst0_snd . . . . . previous)
we proved fsubst0 i u0 c t c x1
by (H3 . . . H4 . . previous)
arity g c x1 a0
end of h2
by (arity_cast . . . . h1 . h2)
we proved arity g c (THead (Flat Cast) x0 x1) a0
by (eq_ind_r . . . previous . H11)
arity g c t2 a0
arity g c t2 a0
arity g c t2 a0
arity g c2 t2 a0
arity g c2 t2 a0
case or3_intro1 : H7:land (eq T (THead (Flat Cast) u t) t2) (csubst0 i u0 c c2) ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H7 to prove arity g c2 t2 a0
case conj : H8:eq T (THead (Flat Cast) u t) t2 H9:csubst0 i u0 c c2 ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H8 to prove arity g c2 t2 a0
case refl_equal : ⇒
the thesis becomes arity g c2 (THead (Flat Cast) u t) a0
(h1)
by (fsubst0_fst . . . . . H9)
we proved fsubst0 i u0 c u c2 u
by (H1 . . . H4 . . previous)
arity g c2 u (asucc g a0)
end of h1
(h2)
by (fsubst0_fst . . . . . H9)
we proved fsubst0 i u0 c t c2 t
by (H3 . . . H4 . . previous)
arity g c2 t a0
end of h2
by (arity_cast . . . . h1 . h2)
arity g c2 (THead (Flat Cast) u t) a0
arity g c2 t2 a0
arity g c2 t2 a0
case or3_intro2 : H7:land (subst0 i u0 (THead (Flat Cast) u t) t2) (csubst0 i u0 c c2) ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H7 to prove arity g c2 t2 a0
case conj : H8:subst0 i u0 (THead (Flat Cast) u t) t2 H9:csubst0 i u0 c c2 ⇒
the thesis becomes arity g c2 t2 a0
by (subst0_gen_head . . . . . . H8)
we proved
or3
ex2 T λu2:T.eq T t2 (THead (Flat Cast) u2 t) λu2:T.subst0 i u0 u u2
ex2 T λt2:T.eq T t2 (THead (Flat Cast) u t2) λt2:T.subst0 (s (Flat Cast) i) u0 t t2
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Flat Cast) u2 t2)
λu2:T.λ:T.subst0 i u0 u u2
λ:T.λt2:T.subst0 (s (Flat Cast) i) u0 t t2
we proceed by induction on the previous result to prove arity g c2 t2 a0
case or3_intro0 : H10:ex2 T λu2:T.eq T t2 (THead (Flat Cast) u2 t) λu2:T.subst0 i u0 u u2 ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H10 to prove arity g c2 t2 a0
case ex_intro2 : x:T H11:eq T t2 (THead (Flat Cast) x t) H12:subst0 i u0 u x ⇒
the thesis becomes arity g c2 t2 a0
(h1)
by (fsubst0_both . . . . . H12 . H9)
we proved fsubst0 i u0 c u c2 x
by (H1 . . . H4 . . previous)
arity g c2 x (asucc g a0)
end of h1
(h2)
by (fsubst0_fst . . . . . H9)
we proved fsubst0 i u0 c t c2 t
by (H3 . . . H4 . . previous)
arity g c2 t a0
end of h2
by (arity_cast . . . . h1 . h2)
we proved arity g c2 (THead (Flat Cast) x t) a0
by (eq_ind_r . . . previous . H11)
arity g c2 t2 a0
arity g c2 t2 a0
case or3_intro1 : H10:ex2 T λt3:T.eq T t2 (THead (Flat Cast) u t3) λt3:T.subst0 (s (Flat Cast) i) u0 t t3 ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H10 to prove arity g c2 t2 a0
case ex_intro2 : x:T H11:eq T t2 (THead (Flat Cast) u x) H12:subst0 (s (Flat Cast) i) u0 t x ⇒
the thesis becomes arity g c2 t2 a0
(h1)
by (fsubst0_fst . . . . . H9)
we proved fsubst0 i u0 c u c2 u
by (H1 . . . H4 . . previous)
arity g c2 u (asucc g a0)
end of h1
(h2)
consider H12
we proved subst0 (s (Flat Cast) i) u0 t x
that is equivalent to subst0 i u0 t x
by (fsubst0_both . . . . . previous . H9)
we proved fsubst0 i u0 c t c2 x
by (H3 . . . H4 . . previous)
arity g c2 x a0
end of h2
by (arity_cast . . . . h1 . h2)
we proved arity g c2 (THead (Flat Cast) u x) a0
by (eq_ind_r . . . previous . H11)
arity g c2 t2 a0
arity g c2 t2 a0
case or3_intro2 : H10:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt3:T.subst0 (s (Flat Cast) i) u0 t t3 ⇒
the thesis becomes arity g c2 t2 a0
we proceed by induction on H10 to prove arity g c2 t2 a0
case ex3_2_intro : x0:T x1:T H11:eq T t2 (THead (Flat Cast) x0 x1) H12:subst0 i u0 u x0 H13:subst0 (s (Flat Cast) i) u0 t x1 ⇒
the thesis becomes arity g c2 t2 a0
(h1)
by (fsubst0_both . . . . . H12 . H9)
we proved fsubst0 i u0 c u c2 x0
by (H1 . . . H4 . . previous)
arity g c2 x0 (asucc g a0)
end of h1
(h2)
consider H13
we proved subst0 (s (Flat Cast) i) u0 t x1
that is equivalent to subst0 i u0 t x1
by (fsubst0_both . . . . . previous . H9)
we proved fsubst0 i u0 c t c2 x1
by (H3 . . . H4 . . previous)
arity g c2 x1 a0
end of h2
by (arity_cast . . . . h1 . h2)
we proved arity g c2 (THead (Flat Cast) x0 x1) a0
by (eq_ind_r . . . previous . H11)
arity g c2 t2 a0
arity g c2 t2 a0
arity g c2 t2 a0
arity g c2 t2 a0
we proved arity g c2 t2 a0
∀d1:C
.∀u0:T
.∀i:nat
.∀H4:getl i c (CHead d1 (Bind Abbr) u0)
.∀c2:C.∀t2:T.∀H5:(fsubst0 i u0 c (THead (Flat Cast) u t) c2 t2).(arity g c2 t2 a0)
case arity_repl : c:C t:T a1:A :arity g c t a1 a2:A H2:leq g a1 a2 ⇒
the thesis becomes ∀d1:C.∀u:T.∀i:nat.∀H3:(getl i c (CHead d1 (Bind Abbr) u)).∀c2:C.∀t2:T.∀H4:(fsubst0 i u c t c2 t2).(arity g c2 t2 a2)
(H1) by induction hypothesis we know
∀d1:C
.∀u:T
.∀i:nat
.getl i c (CHead d1 (Bind Abbr) u)
→∀c2:C.∀t2:T.(fsubst0 i u c t c2 t2)→(arity g c2 t2 a1)
assume d1: C
assume u: T
assume i: nat
suppose H3: getl i c (CHead d1 (Bind Abbr) u)
assume c2: C
assume t2: T
suppose H4: fsubst0 i u c t c2 t2
(H_x)
by (fsubst0_gen_base . . . . . . H4)
or3
land (eq C c c2) (subst0 i u t t2)
land (eq T t t2) (csubst0 i u c c2)
land (subst0 i u t t2) (csubst0 i u c c2)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove arity g c2 t2 a2
case or3_intro0 : H6:land (eq C c c2) (subst0 i u t t2) ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H6 to prove arity g c2 t2 a2
case conj : H7:eq C c c2 H8:subst0 i u t t2 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H7 to prove arity g c2 t2 a2
case refl_equal : ⇒
the thesis becomes arity g c t2 a2
by (fsubst0_snd . . . . . H8)
we proved fsubst0 i u c t c t2
by (H1 . . . H3 . . previous)
we proved arity g c t2 a1
by (arity_repl . . . . previous . H2)
arity g c t2 a2
arity g c2 t2 a2
arity g c2 t2 a2
case or3_intro1 : H6:land (eq T t t2) (csubst0 i u c c2) ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H6 to prove arity g c2 t2 a2
case conj : H7:eq T t t2 H8:csubst0 i u c c2 ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H7 to prove arity g c2 t2 a2
case refl_equal : ⇒
the thesis becomes arity g c2 t a2
by (fsubst0_fst . . . . . H8)
we proved fsubst0 i u c t c2 t
by (H1 . . . H3 . . previous)
we proved arity g c2 t a1
by (arity_repl . . . . previous . H2)
arity g c2 t a2
arity g c2 t2 a2
arity g c2 t2 a2
case or3_intro2 : H6:land (subst0 i u t t2) (csubst0 i u c c2) ⇒
the thesis becomes arity g c2 t2 a2
we proceed by induction on H6 to prove arity g c2 t2 a2
case conj : H7:subst0 i u t t2 H8:csubst0 i u c c2 ⇒
the thesis becomes arity g c2 t2 a2
by (fsubst0_both . . . . . H7 . H8)
we proved fsubst0 i u c t c2 t2
by (H1 . . . H3 . . previous)
we proved arity g c2 t2 a1
by (arity_repl . . . . previous . H2)
arity g c2 t2 a2
arity g c2 t2 a2
we proved arity g c2 t2 a2
∀d1:C.∀u:T.∀i:nat.∀H3:(getl i c (CHead d1 (Bind Abbr) u)).∀c2:C.∀t2:T.∀H4:(fsubst0 i u c t c2 t2).(arity g c2 t2 a2)
we proved
∀d1:C
.∀u:T
.∀i:nat
.(getl i c1 (CHead d1 (Bind Abbr) u))→∀c2:C.∀t2:T.(fsubst0 i u c1 t1 c2 t2)→(arity g c2 t2 a)
we proved
∀g:G
.∀c1:C
.∀t1:T
.∀a:A
.arity g c1 t1 a
→∀d1:C
.∀u:T
.∀i:nat
.(getl i c1 (CHead d1 (Bind Abbr) u))→∀c2:C.∀t2:T.(fsubst0 i u c1 t1 c2 t2)→(arity g c2 t2 a)