DEFINITION csuba_getl_abst()
TYPE =
∀g:G
.∀c1:C
.∀d1:C
.∀u1:T
.∀i:nat
.getl i c1 (CHead d1 (Bind Abst) u1)
→∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
BODY =
assume g: G
assume c1: C
assume d1: C
assume u1: T
assume i: nat
suppose H: getl i c1 (CHead d1 (Bind Abst) u1)
(H0)
by (getl_gen_all . . . H)
ex2 C λe:C.drop i O c1 e λe:C.clear e (CHead d1 (Bind Abst) u1)
end of H0
we proceed by induction on H0 to prove
∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
case ex_intro2 : x:C H1:drop i O c1 x H2:clear x (CHead d1 (Bind Abst) u1) ⇒
the thesis becomes
∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
assume n: nat
suppose : drop i O c1 (CSort n)
suppose H4: clear (CSort n) (CHead d1 (Bind Abst) u1)
by (clear_gen_sort . . H4 .)
we proved
∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
drop i O c1 (CSort n)
→∀H4:clear (CSort n) (CHead d1 (Bind Abst) u1)
.∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
assume x0: C
suppose :
drop i O c1 x0
→(clear x0 (CHead d1 (Bind Abst) u1)
→∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a))
assume k: K
assume t: T
suppose H3: drop i O c1 (CHead x0 k t)
suppose H4: clear (CHead x0 k t) (CHead d1 (Bind Abst) u1)
assume b: B
suppose H5: drop i O c1 (CHead x0 (Bind b) t)
suppose H6: clear (CHead x0 (Bind b) t) (CHead d1 (Bind Abst) u1)
(H7)
by (clear_gen_bind . . . . H6)
we proved eq C (CHead d1 (Bind Abst) u1) (CHead x0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Abst) u1 OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead x0 (Bind b) t OF CSort ⇒d1 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead d1 (Bind Abst) u1)
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead x0 (Bind b) t)
end of H7
(h1)
(H8)
by (clear_gen_bind . . . . H6)
we proved eq C (CHead d1 (Bind Abst) u1) (CHead x0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind Abst) u1 OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
<λ:C.B>
CASE CHead x0 (Bind b) t OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
CHead d1 (Bind Abst) u1
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
CHead x0 (Bind b) t
end of H8
(h1)
(H9)
by (clear_gen_bind . . . . H6)
we proved eq C (CHead d1 (Bind Abst) u1) (CHead x0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d1 (Bind Abst) u1 OF CSort ⇒u1 | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind b) t OF CSort ⇒u1 | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u1 | CHead t0⇒t0 (CHead d1 (Bind Abst) u1)
λe:C.<λ:C.T> CASE e OF CSort ⇒u1 | CHead t0⇒t0 (CHead x0 (Bind b) t)
end of H9
suppose H10: eq B Abst b
suppose H11: eq C d1 x0
assume c2: C
suppose H12: csuba g c1 c2
(H13)
consider H9
we proved
eq
T
<λ:C.T> CASE CHead d1 (Bind Abst) u1 OF CSort ⇒u1 | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind b) t OF CSort ⇒u1 | CHead t0⇒t0
that is equivalent to eq T u1 t
by (eq_ind_r . . . H5 . previous)
drop i O c1 (CHead x0 (Bind b) u1)
end of H13
(H14)
by (eq_ind_r . . . H13 . H10)
drop i O c1 (CHead x0 (Bind Abst) u1)
end of H14
(H15)
by (eq_ind_r . . . H14 . H11)
drop i O c1 (CHead d1 (Bind Abst) u1)
end of H15
(H16)
by (csuba_drop_abst . . . . H15 . . H12)
or
ex2 C λd2:C.drop i O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop i O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
end of H16
we proceed by induction on H16 to prove
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case or_introl : H17:ex2 C λd2:C.drop i O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2 ⇒
the thesis becomes
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
we proceed by induction on H17 to prove
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case ex_intro2 : x1:C H18:drop i O c2 (CHead x1 (Bind Abst) u1) H19:csuba g d1 x1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
by (clear_bind . . .)
we proved clear (CHead x1 (Bind Abst) u1) (CHead x1 (Bind Abst) u1)
by (getl_intro . . . . H18 previous)
we proved getl i c2 (CHead x1 (Bind Abst) u1)
by (ex_intro2 . . . . previous H19)
we proved ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
by (or_introl . . previous)
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case or_intror : H17:ex4_3 C T A λd2:C.λu2:T.λ:A.drop i O c2 (CHead d2 (Bind Abbr) u2) λd2:C.λ:T.λ:A.csuba g d1 d2 λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a) λd2:C.λu2:T.λa:A.arity g d2 u2 a ⇒
the thesis becomes
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
we proceed by induction on H17 to prove
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case ex4_3_intro : x1:C x2:T x3:A H18:drop i O c2 (CHead x1 (Bind Abbr) x2) H19:csuba g d1 x1 H20:arity g d1 u1 (asucc g x3) H21:arity g x1 x2 x3 ⇒
the thesis becomes
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
by (clear_bind . . .)
we proved clear (CHead x1 (Bind Abbr) x2) (CHead x1 (Bind Abbr) x2)
by (getl_intro . . . . H18 previous)
we proved getl i c2 (CHead x1 (Bind Abbr) x2)
by (ex4_3_intro . . . . . . . . . . previous H19 H20 H21)
we proved
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
by (or_intror . . previous)
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
we proved
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
eq B Abst b
→(eq C d1 x0
→∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a))
end of h1
(h2)
consider H8
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind Abst) u1 OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
<λ:C.B>
CASE CHead x0 (Bind b) t OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
eq B Abst b
end of h2
by (h1 h2)
eq C d1 x0
→∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
end of h1
(h2)
consider H7
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Abst) u1 OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead x0 (Bind b) t OF CSort ⇒d1 | CHead c ⇒c
eq C d1 x0
end of h2
by (h1 h2)
we proved
∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
∀H5:drop i O c1 (CHead x0 (Bind b) t)
.∀H6:clear (CHead x0 (Bind b) t) (CHead d1 (Bind Abst) u1)
.∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
assume f: F
suppose H5: drop i O c1 (CHead x0 (Flat f) t)
suppose H6: clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abst) u1)
(H7) consider H5
we proceed by induction on i to prove
∀x1:C
.drop i O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g x1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
case O : ⇒
the thesis becomes
∀x1:C
.drop O O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g x1 c2
→(or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
assume x1: C
suppose H8: drop O O x1 (CHead x0 (Flat f) t)
assume c2: C
suppose H9: csuba g x1 c2
(H10)
by (drop_gen_refl . . H8)
we proved eq C x1 (CHead x0 (Flat f) t)
we proceed by induction on the previous result to prove csuba g (CHead x0 (Flat f) t) c2
case refl_equal : ⇒
the thesis becomes the hypothesis H9
csuba g (CHead x0 (Flat f) t) c2
end of H10
(H_y)
by (clear_gen_flat . . . . H6)
we proved clear x0 (CHead d1 (Bind Abst) u1)
by (clear_flat . . previous . .)
clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abst) u1)
end of H_y
(H11)
by (csuba_clear_conf . . . H10 . H_y)
ex2 C λe2:C.csuba g (CHead d1 (Bind Abst) u1) e2 λe2:C.clear c2 e2
end of H11
we proceed by induction on H11 to prove
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case ex_intro2 : x2:C H12:csuba g (CHead d1 (Bind Abst) u1) x2 H13:clear c2 x2 ⇒
the thesis becomes
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
(H_x)
by (csuba_gen_abst . . . . H12)
or
ex2 C λd2:C.eq C x2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C x2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
end of H_x
(H14) consider H_x
we proceed by induction on H14 to prove
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case or_introl : H15:ex2 C λd2:C.eq C x2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2 ⇒
the thesis becomes
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
we proceed by induction on H15 to prove
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case ex_intro2 : x3:C H16:eq C x2 (CHead x3 (Bind Abst) u1) H17:csuba g d1 x3 ⇒
the thesis becomes
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
(H18)
we proceed by induction on H16 to prove clear c2 (CHead x3 (Bind Abst) u1)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
clear c2 (CHead x3 (Bind Abst) u1)
end of H18
by (drop_refl .)
we proved drop O O c2 c2
by (getl_intro . . . . previous H18)
we proved getl O c2 (CHead x3 (Bind Abst) u1)
by (ex_intro2 . . . . previous H17)
we proved ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
by (or_introl . . previous)
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case or_intror : H15:ex4_3 C T A λd2:C.λu2:T.λ:A.eq C x2 (CHead d2 (Bind Abbr) u2) λd2:C.λ:T.λ:A.csuba g d1 d2 λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a) λd2:C.λu2:T.λa:A.arity g d2 u2 a ⇒
the thesis becomes
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
we proceed by induction on H15 to prove
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case ex4_3_intro : x3:C x4:T x5:A H16:eq C x2 (CHead x3 (Bind Abbr) x4) H17:csuba g d1 x3 H18:arity g d1 u1 (asucc g x5) H19:arity g x3 x4 x5 ⇒
the thesis becomes
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
(H20)
we proceed by induction on H16 to prove clear c2 (CHead x3 (Bind Abbr) x4)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
clear c2 (CHead x3 (Bind Abbr) x4)
end of H20
by (drop_refl .)
we proved drop O O c2 c2
by (getl_intro . . . . previous H20)
we proved getl O c2 (CHead x3 (Bind Abbr) x4)
by (ex4_3_intro . . . . . . . . . . previous H17 H18 H19)
we proved
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
by (or_intror . . previous)
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
we proved
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
∀x1:C
.drop O O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g x1 c2
→(or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl O c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
case S : n:nat ⇒
the thesis becomes
∀x1:C
.∀H9:drop (S n) O x1 (CHead x0 (Flat f) t)
.∀c2:C
.∀H10:csuba g x1 c2
.or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
(H8) by induction hypothesis we know
∀x1:C
.drop n O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g x1 c2
→(or
ex2 C λd2:C.getl n c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl n c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
assume x1: C
suppose H9: drop (S n) O x1 (CHead x0 (Flat f) t)
assume c2: C
suppose H10: csuba g x1 c2
(H11)
by (drop_clear . . . H9)
ex2_3
B
C
T
λb:B.λe:C.λv:T.clear x1 (CHead e (Bind b) v)
λ:B.λe:C.λ:T.drop n O e (CHead x0 (Flat f) t)
end of H11
we proceed by induction on H11 to prove
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case ex2_3_intro : x2:B x3:C x4:T H12:clear x1 (CHead x3 (Bind x2) x4) H13:drop n O x3 (CHead x0 (Flat f) t) ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
(H14)
by (csuba_clear_conf . . . H10 . H12)
ex2 C λe2:C.csuba g (CHead x3 (Bind x2) x4) e2 λe2:C.clear c2 e2
end of H14
we proceed by induction on H14 to prove
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case ex_intro2 : x5:C H15:csuba g (CHead x3 (Bind x2) x4) x5 H16:clear c2 x5 ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
(H_x)
by (csuba_gen_bind . . . . . H15)
ex2_3 B C T λb2:B.λe2:C.λv2:T.eq C x5 (CHead e2 (Bind b2) v2) λ:B.λe2:C.λ:T.csuba g x3 e2
end of H_x
(H17) consider H_x
we proceed by induction on H17 to prove
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case ex2_3_intro : x6:B x7:C x8:T H18:eq C x5 (CHead x7 (Bind x6) x8) H19:csuba g x3 x7 ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
(H20)
we proceed by induction on H18 to prove clear c2 (CHead x7 (Bind x6) x8)
case refl_equal : ⇒
the thesis becomes the hypothesis H16
clear c2 (CHead x7 (Bind x6) x8)
end of H20
(H21)
by (H8 . H13 . H19)
or
ex2 C λd2:C.getl n x7 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl n x7 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
end of H21
we proceed by induction on H21 to prove
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case or_introl : H22:ex2 C λd2:C.getl n x7 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2 ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
we proceed by induction on H22 to prove
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case ex_intro2 : x9:C H23:getl n x7 (CHead x9 (Bind Abst) u1) H24:csuba g d1 x9 ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
by (getl_clear_bind . . . . H20 . . H23)
we proved getl (S n) c2 (CHead x9 (Bind Abst) u1)
by (ex_intro2 . . . . previous H24)
we proved ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
by (or_introl . . previous)
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case or_intror : H22:ex4_3 C T A λd2:C.λu2:T.λ:A.getl n x7 (CHead d2 (Bind Abbr) u2) λd2:C.λ:T.λ:A.csuba g d1 d2 λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a) λd2:C.λu2:T.λa:A.arity g d2 u2 a ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
we proceed by induction on H22 to prove
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
case ex4_3_intro : x9:C x10:T x11:A H23:getl n x7 (CHead x9 (Bind Abbr) x10) H24:csuba g d1 x9 H25:arity g d1 u1 (asucc g x11) H26:arity g x9 x10 x11 ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
by (getl_clear_bind . . . . H20 . . H23)
we proved getl (S n) c2 (CHead x9 (Bind Abbr) x10)
by (ex4_3_intro . . . . . . . . . . previous H24 H25 H26)
we proved
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
by (or_intror . . previous)
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
we proved
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
∀x1:C
.∀H9:drop (S n) O x1 (CHead x0 (Flat f) t)
.∀c2:C
.∀H10:csuba g x1 c2
.or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl (S n) c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
we proved
∀x1:C
.drop i O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g x1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
by (unintro . . . previous H7)
we proved
∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
∀H5:drop i O c1 (CHead x0 (Flat f) t)
.∀H6:clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abst) u1)
.∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
by (previous . H3 H4)
we proved
∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
∀H3:drop i O c1 (CHead x0 k t)
.∀H4:clear (CHead x0 k t) (CHead d1 (Bind Abst) u1)
.∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
by (previous . H1 H2)
∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
we proved
∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)
we proved
∀g:G
.∀c1:C
.∀d1:C
.∀u1:T
.∀i:nat
.getl i c1 (CHead d1 (Bind Abst) u1)
→∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d1 d2
λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a)