DEFINITION getl_csubst1()
TYPE =
∀d:nat
.∀c:C
.∀e:C
.∀u:T
.getl d c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 d u c a0 λa0:C.λa:C.drop (S O) d a0 a
BODY =
assume d: nat
we proceed by induction on d to prove
∀c:C
.∀e:C
.∀u:T
.getl d c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 d u c a0 λa0:C.λa:C.drop (S O) d a0 a
case O : ⇒
the thesis becomes
∀c:C
.∀e:C
.∀u:T
.getl O c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 O u c a0 λa0:C.λa:C.drop (S O) O a0 a
assume c: C
we proceed by induction on c to prove
∀e:C
.∀u:T
.getl O c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 O u c a0 λa0:C.λa:C.drop (S O) O a0 a
case CSort : n:nat ⇒
the thesis becomes
∀e:C
.∀u:T
.∀H:getl O (CSort n) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 O u (CSort n) a0 λa0:C.λa:C.drop (S O) O a0 a
assume e: C
assume u: T
suppose H: getl O (CSort n) (CHead e (Bind Abbr) u)
by (getl_gen_sort . . . H .)
we proved ex2_2 C C λa0:C.λ:C.csubst1 O u (CSort n) a0 λa0:C.λa:C.drop (S O) O a0 a
∀e:C
.∀u:T
.∀H:getl O (CSort n) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 O u (CSort n) a0 λa0:C.λa:C.drop (S O) O a0 a
case CHead ⇒
we need to prove
∀c0:C
.∀e:C
.∀u:T
.getl O c0 (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 O u c0 a0 λa0:C.λa:C.drop (S O) O a0 a
→∀k:K
.∀t:T
.∀e:C
.∀u:T
.getl O (CHead c0 k t) (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 k t) a0 λa0:C.λa:C.drop (S O) O a0 a
assume c0: C
suppose H:
∀e:C
.∀u:T
.getl O c0 (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 O u c0 a0 λa0:C.λa:C.drop (S O) O a0 a
assume k: K
we proceed by induction on k to prove
∀t:T
.∀e:C
.∀u:T
.getl O (CHead c0 k t) (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 k t) a0 λa0:C.λa:C.drop (S O) O a0 a
case Bind : b:B ⇒
the thesis becomes
∀t:T
.∀e:C
.∀u:T
.∀H0:getl O (CHead c0 (Bind b) t) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) O a0 a
assume t: T
assume e: C
assume u: T
suppose H0: getl O (CHead c0 (Bind b) t) (CHead e (Bind Abbr) u)
(H1)
by (getl_gen_O . . H0)
we proved clear (CHead c0 (Bind b) t) (CHead e (Bind Abbr) u)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead e (Bind Abbr) u) (CHead c0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead e (Bind Abbr) u OF CSort ⇒e | CHead c1 ⇒c1
<λ:C.C> CASE CHead c0 (Bind b) t OF CSort ⇒e | CHead c1 ⇒c1
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒e | CHead c1 ⇒c1 (CHead e (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒e | CHead c1 ⇒c1 (CHead c0 (Bind b) t)
end of H1
(h1)
(H2)
by (getl_gen_O . . H0)
we proved clear (CHead c0 (Bind b) t) (CHead e (Bind Abbr) u)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead e (Bind Abbr) u) (CHead c0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead e (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c0 (Bind b) t OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
eq
B
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
CHead e (Bind Abbr) u
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
CHead c0 (Bind b) t
end of H2
(h1)
(H3)
by (getl_gen_O . . H0)
we proved clear (CHead c0 (Bind b) t) (CHead e (Bind Abbr) u)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead e (Bind Abbr) u) (CHead c0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead e (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead c0 (Bind b) t OF CSort ⇒u | CHead t0⇒t0
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t0⇒t0 (CHead e (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t0⇒t0 (CHead c0 (Bind b) t)
end of H3
suppose H4: eq B Abbr b
suppose : eq C e c0
(h1)
we proceed by induction on H4 to prove ex2_2 C C λa0:C.λ:C.csubst1 O t (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) O a0 a
case refl_equal : ⇒
the thesis becomes ex2_2 C C λa0:C.λ:C.csubst1 O t (CHead c0 (Bind Abbr) t) a0 λa0:C.λa:C.drop (S O) O a0 a
(h1)
by (csubst1_refl . . .)
csubst1 O t (CHead c0 (Bind Abbr) t) (CHead c0 (Bind Abbr) t)
end of h1
(h2)
by (drop_refl .)
we proved drop O O c0 c0
that is equivalent to drop (r (Bind Abbr) O) O c0 c0
by (drop_drop . . . . previous .)
drop (S O) O (CHead c0 (Bind Abbr) t) c0
end of h2
by (ex2_2_intro . . . . . . h1 h2)
ex2_2 C C λa0:C.λ:C.csubst1 O t (CHead c0 (Bind Abbr) t) a0 λa0:C.λa:C.drop (S O) O a0 a
ex2_2 C C λa0:C.λ:C.csubst1 O t (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) O a0 a
end of h1
(h2)
consider H3
we proved
eq
T
<λ:C.T> CASE CHead e (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead c0 (Bind b) t OF CSort ⇒u | CHead t0⇒t0
eq T u t
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) O a0 a
eq B Abbr b
→(eq C e c0
→ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) O a0 a)
end of h1
(h2)
consider H2
we proved
eq
B
<λ:C.B>
CASE CHead e (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c0 (Bind b) t OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
eq B Abbr b
end of h2
by (h1 h2)
eq C e c0
→ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) O a0 a
end of h1
(h2)
consider H1
we proved
eq
C
<λ:C.C> CASE CHead e (Bind Abbr) u OF CSort ⇒e | CHead c1 ⇒c1
<λ:C.C> CASE CHead c0 (Bind b) t OF CSort ⇒e | CHead c1 ⇒c1
eq C e c0
end of h2
by (h1 h2)
we proved ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) O a0 a
∀t:T
.∀e:C
.∀u:T
.∀H0:getl O (CHead c0 (Bind b) t) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) O a0 a
case Flat : f:F ⇒
the thesis becomes
∀t:T
.∀e:C
.∀u:T
.∀H0:getl O (CHead c0 (Flat f) t) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) O a0 a
assume t: T
assume e: C
assume u: T
suppose H0: getl O (CHead c0 (Flat f) t) (CHead e (Bind Abbr) u)
(H_x)
by (subst1_ex . . .)
ex T λt2:T.subst1 O u t (lift (S O) O t2)
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) O a0 a
case ex_intro : x:T H2:subst1 O u t (lift (S O) O x) ⇒
the thesis becomes ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) O a0 a
(H3)
(h1)
by (drop_refl .)
drop O O c0 c0
end of h1
(h2)
by (getl_gen_O . . H0)
we proved clear (CHead c0 (Flat f) t) (CHead e (Bind Abbr) u)
by (clear_gen_flat . . . . previous)
clear c0 (CHead e (Bind Abbr) u)
end of h2
by (getl_intro . . . . h1 h2)
we proved getl O c0 (CHead e (Bind Abbr) u)
by (H . . previous)
ex2_2 C C λa0:C.λ:C.csubst1 O u c0 a0 λa0:C.λa:C.drop (S O) O a0 a
end of H3
we proceed by induction on H3 to prove ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) O a0 a
case ex2_2_intro : x0:C x1:C H4:csubst1 O u c0 x0 H5:drop (S O) O x0 x1 ⇒
the thesis becomes ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) O a0 a
(h1)
by (csubst1_flat . . . . . H2 . . H4)
csubst1 O u (CHead c0 (Flat f) t) (CHead x0 (Flat f) (lift (S O) O x))
end of h1
(h2)
consider H5
we proved drop (S O) O x0 x1
that is equivalent to drop (r (Flat f) O) O x0 x1
by (drop_drop . . . . previous .)
drop (S O) O (CHead x0 (Flat f) (lift (S O) O x)) x1
end of h2
by (ex2_2_intro . . . . . . h1 h2)
ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) O a0 a
ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) O a0 a
we proved ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) O a0 a
∀t:T
.∀e:C
.∀u:T
.∀H0:getl O (CHead c0 (Flat f) t) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) O a0 a
we proved
∀t:T
.∀e:C
.∀u:T
.getl O (CHead c0 k t) (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 k t) a0 λa0:C.λa:C.drop (S O) O a0 a
∀c0:C
.∀e:C
.∀u:T
.getl O c0 (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 O u c0 a0 λa0:C.λa:C.drop (S O) O a0 a
→∀k:K
.∀t:T
.∀e:C
.∀u:T
.getl O (CHead c0 k t) (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 O u (CHead c0 k t) a0 λa0:C.λa:C.drop (S O) O a0 a
we proved
∀e:C
.∀u:T
.getl O c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 O u c a0 λa0:C.λa:C.drop (S O) O a0 a
∀c:C
.∀e:C
.∀u:T
.getl O c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 O u c a0 λa0:C.λa:C.drop (S O) O a0 a
case S : n:nat ⇒
the thesis becomes
∀c:C
.∀e:C
.∀u:T
.getl (S n) c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 (S n) u c a0 λa0:C.λa:C.drop (S O) (S n) a0 a
(H) by induction hypothesis we know
∀c:C
.∀e:C
.∀u:T
.getl n c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 n u c a0 λa0:C.λa:C.drop (S O) n a0 a
assume c: C
we proceed by induction on c to prove
∀e:C
.∀u:T
.getl (S n) c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 (S n) u c a0 λa0:C.λa:C.drop (S O) (S n) a0 a
case CSort : n0:nat ⇒
the thesis becomes
∀e:C
.∀u:T
.∀H0:getl (S n) (CSort n0) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CSort n0) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
assume e: C
assume u: T
suppose H0: getl (S n) (CSort n0) (CHead e (Bind Abbr) u)
by (getl_gen_sort . . . H0 .)
we proved ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CSort n0) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
∀e:C
.∀u:T
.∀H0:getl (S n) (CSort n0) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CSort n0) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
case CHead ⇒
we need to prove
∀c0:C
.∀e:C
.∀u:T
.getl (S n) c0 (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 (S n) u c0 a0 λa0:C.λa:C.drop (S O) (S n) a0 a
→∀k:K
.∀t:T
.∀e:C
.∀u:T
.getl (S n) (CHead c0 k t) (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 k t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
assume c0: C
suppose H0:
∀e:C
.∀u:T
.getl (S n) c0 (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 (S n) u c0 a0 λa0:C.λa:C.drop (S O) (S n) a0 a
assume k: K
we proceed by induction on k to prove
∀t:T
.∀e:C
.∀u:T
.getl (S n) (CHead c0 k t) (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 k t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
case Bind : b:B ⇒
the thesis becomes
∀t:T
.∀e:C
.∀u:T
.∀H1:getl (S n) (CHead c0 (Bind b) t) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
assume t: T
assume e: C
assume u: T
suppose H1: getl (S n) (CHead c0 (Bind b) t) (CHead e (Bind Abbr) u)
(H_x)
by (subst1_ex . . .)
ex T λt2:T.subst1 n u t (lift (S O) n t2)
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
case ex_intro : x:T H3:subst1 n u t (lift (S O) n x) ⇒
the thesis becomes ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
(H4)
by (getl_gen_S . . . . . H1)
we proved getl (r (Bind b) n) c0 (CHead e (Bind Abbr) u)
that is equivalent to getl n c0 (CHead e (Bind Abbr) u)
by (H . . . previous)
ex2_2 C C λa0:C.λ:C.csubst1 n u c0 a0 λa0:C.λa:C.drop (S O) n a0 a
end of H4
we proceed by induction on H4 to prove ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
case ex2_2_intro : x0:C x1:C H5:csubst1 n u c0 x0 H6:drop (S O) n x0 x1 ⇒
the thesis becomes ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
(h1)
by (csubst1_bind . . . . . H3 . . H5)
csubst1
S n
u
CHead c0 (Bind b) t
CHead x0 (Bind b) (lift (S O) n x)
end of h1
(h2)
by (drop_skip_bind . . . . H6 . .)
drop
S O
S n
CHead x0 (Bind b) (lift (S O) n x)
CHead x1 (Bind b) x
end of h2
by (ex2_2_intro . . . . . . h1 h2)
ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
we proved ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
∀t:T
.∀e:C
.∀u:T
.∀H1:getl (S n) (CHead c0 (Bind b) t) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Bind b) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
case Flat : f:F ⇒
the thesis becomes
∀t:T
.∀e:C
.∀u:T
.∀H1:getl (S n) (CHead c0 (Flat f) t) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
assume t: T
assume e: C
assume u: T
suppose H1: getl (S n) (CHead c0 (Flat f) t) (CHead e (Bind Abbr) u)
(H_x)
by (subst1_ex . . .)
ex T λt2:T.subst1 (S n) u t (lift (S O) (S n) t2)
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
case ex_intro : x:T H3:subst1 (S n) u t (lift (S O) (S n) x) ⇒
the thesis becomes ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
(H4)
by (getl_gen_S . . . . . H1)
we proved getl (r (Flat f) n) c0 (CHead e (Bind Abbr) u)
that is equivalent to getl (S n) c0 (CHead e (Bind Abbr) u)
by (H0 . . previous)
ex2_2 C C λa0:C.λ:C.csubst1 (S n) u c0 a0 λa0:C.λa:C.drop (S O) (S n) a0 a
end of H4
we proceed by induction on H4 to prove ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
case ex2_2_intro : x0:C x1:C H5:csubst1 (S n) u c0 x0 H6:drop (S O) (S n) x0 x1 ⇒
the thesis becomes ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
(h1)
by (csubst1_flat . . . . . H3 . . H5)
csubst1
S n
u
CHead c0 (Flat f) t
CHead x0 (Flat f) (lift (S O) (S n) x)
end of h1
(h2)
by (drop_skip_flat . . . . H6 . .)
drop
S O
S n
CHead x0 (Flat f) (lift (S O) (S n) x)
CHead x1 (Flat f) x
end of h2
by (ex2_2_intro . . . . . . h1 h2)
ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
we proved ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
∀t:T
.∀e:C
.∀u:T
.∀H1:getl (S n) (CHead c0 (Flat f) t) (CHead e (Bind Abbr) u)
.ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 (Flat f) t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
we proved
∀t:T
.∀e:C
.∀u:T
.getl (S n) (CHead c0 k t) (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 k t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
∀c0:C
.∀e:C
.∀u:T
.getl (S n) c0 (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 (S n) u c0 a0 λa0:C.λa:C.drop (S O) (S n) a0 a
→∀k:K
.∀t:T
.∀e:C
.∀u:T
.getl (S n) (CHead c0 k t) (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 (S n) u (CHead c0 k t) a0 λa0:C.λa:C.drop (S O) (S n) a0 a
we proved
∀e:C
.∀u:T
.getl (S n) c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 (S n) u c a0 λa0:C.λa:C.drop (S O) (S n) a0 a
∀c:C
.∀e:C
.∀u:T
.getl (S n) c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 (S n) u c a0 λa0:C.λa:C.drop (S O) (S n) a0 a
we proved
∀c:C
.∀e:C
.∀u:T
.getl d c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 d u c a0 λa0:C.λa:C.drop (S O) d a0 a
we proved
∀d:nat
.∀c:C
.∀e:C
.∀u:T
.getl d c (CHead e (Bind Abbr) u)
→ex2_2 C C λa0:C.λ:C.csubst1 d u c a0 λa0:C.λa:C.drop (S O) d a0 a