DEFINITION csuba_drop_abst()
TYPE =
∀i:nat
.∀c1:C
.∀d1:C
.∀u1:T
.drop i O c1 (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c1 c2
→(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)
BODY =
assume i: nat
we proceed by induction on i to prove
∀c1:C
.∀d1:C
.∀u1:T
.drop i O c1 (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c1 c2
→(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)
case O : ⇒
the thesis becomes
∀c1:C
.∀d1:C
.∀u1:T
.drop O O c1 (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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 c1: C
assume d1: C
assume u1: T
suppose H: drop O O c1 (CHead d1 (Bind Abst) u1)
assume g: G
assume c2: C
suppose H0: csuba g c1 c2
(H1)
by (drop_gen_refl . . H)
we proved eq C c1 (CHead d1 (Bind Abst) u1)
we proceed by induction on the previous result to prove csuba g (CHead d1 (Bind Abst) u1) c2
case refl_equal : ⇒
the thesis becomes the hypothesis H0
csuba g (CHead d1 (Bind Abst) u1) c2
end of H1
(H_x)
by (csuba_gen_abst . . . . H1)
or
ex2 C λd2:C.eq C c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C 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 H_x
(H2) consider H_x
we proceed by induction on H2 to prove
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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 : H3:ex2 C λd2:C.eq C c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2 ⇒
the thesis becomes
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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 H3 to prove
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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 : x:C H4:eq C c2 (CHead x (Bind Abst) u1) H5:csuba g d1 x ⇒
the thesis becomes
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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 (drop_refl .)
we proved drop O O (CHead x (Bind Abst) u1) (CHead x (Bind Abst) u1)
by (ex_intro2 . . . . previous H5)
we proved
ex2
C
λd2:C.drop O O (CHead x (Bind Abst) u1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
by (or_introl . . previous)
we proved
or
ex2
C
λd2:C.drop O O (CHead x (Bind Abst) u1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O O (CHead x (Bind Abst) u1) (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 (eq_ind_r . . . previous . H4)
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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 : H3:ex4_3 C T A λd2:C.λu2:T.λ:A.eq C 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.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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 H3 to prove
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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 : x0:C x1:T x2:A H4:eq C c2 (CHead x0 (Bind Abbr) x1) H5:csuba g d1 x0 H6:arity g d1 u1 (asucc g x2) H7:arity g x0 x1 x2 ⇒
the thesis becomes
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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 (drop_refl .)
we proved drop O O (CHead x0 (Bind Abbr) x1) (CHead x0 (Bind Abbr) x1)
by (ex4_3_intro . . . . . . . . . . previous H5 H6 H7)
we proved
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O O (CHead x0 (Bind Abbr) x1) (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)
we proved
or
ex2
C
λd2:C.drop O O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O O (CHead x0 (Bind Abbr) x1) (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 (eq_ind_r . . . previous . H4)
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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
∀c1:C
.∀d1:C
.∀u1:T
.drop O O c1 (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop O 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
∀c1:C
.∀d1:C
.∀u1:T
.drop (S n) O c1 (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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) by induction hypothesis we know
∀c1:C
.∀d1:C
.∀u1:T
.drop n O c1 (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.drop n O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop n 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 c1: C
we proceed by induction on c1 to prove
∀d1:C
.∀u1:T
.drop (S n) O c1 (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 CSort : n0:nat ⇒
the thesis becomes
∀d1:C
.∀u1:T
.∀H0:drop (S n) O (CSort n0) (CHead d1 (Bind Abst) u1)
.∀g:G
.∀c2:C
.csuba g (CSort n0) c2
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 d1: C
assume u1: T
suppose H0: drop (S n) O (CSort n0) (CHead d1 (Bind Abst) u1)
assume g: G
assume c2: C
suppose : csuba g (CSort n0) c2
by (drop_gen_sort . . . . H0)
we proved
and3
eq C (CHead d1 (Bind Abst) u1) (CSort n0)
eq nat (S n) O
eq nat O O
we proceed by induction on the previous result to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 and3_intro : :eq C (CHead d1 (Bind Abst) u1) (CSort n0) H3:eq nat (S n) O :eq nat O O ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
(H5)
we proceed by induction on H3 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S n OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S n OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H5
consider H5
we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
∀d1:C
.∀u1:T
.∀H0:drop (S n) O (CSort n0) (CHead d1 (Bind Abst) u1)
.∀g:G
.∀c2:C
.csuba g (CSort n0) c2
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 CHead : c:C k:K t:T ⇒
the thesis becomes
∀d1:C
.∀u1:T
.∀H1:drop (S n) O (CHead c k t) (CHead d1 (Bind Abst) u1)
.∀g:G
.∀c2:C
.∀H2:csuba g (CHead c k t) c2
.or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
(H0) by induction hypothesis we know
∀d1:C
.∀u1:T
.drop (S n) O c (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c c2
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 d1: C
assume u1: T
suppose H1: drop (S n) O (CHead c k t) (CHead d1 (Bind Abst) u1)
assume g: G
assume c2: C
suppose H2: csuba g (CHead c k t) c2
by (drop_gen_drop . . . . . H1)
we proved drop (r k n) O c (CHead d1 (Bind Abst) u1)
assume b: B
suppose H3: csuba g (CHead c (Bind b) t) c2
suppose H4: drop (r (Bind b) n) O c (CHead d1 (Bind Abst) u1)
suppose H5: csuba g (CHead c (Bind Abbr) t) c2
suppose H6: drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abst) u1)
(H_x)
by (csuba_gen_abbr . . . . H5)
ex2 C λd2:C.eq C c2 (CHead d2 (Bind Abbr) t) λd2:C.csuba g c d2
end of H_x
(H7) consider H_x
we proceed by induction on H7 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 : x:C H8:eq C c2 (CHead x (Bind Abbr) t) H9:csuba g c x ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
(H10)
consider H6
we proved drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abst) u1)
that is equivalent to drop n O c (CHead d1 (Bind Abst) u1)
by (H . . . previous . . H9)
or
ex2 C λd2:C.drop n O x (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop n O x (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 H10
we proceed by induction on H10 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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 : H11:ex2 C λd2:C.drop n O x (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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 H11 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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 : x0:C H12:drop n O x (CHead x0 (Bind Abst) u1) H13:csuba g d1 x0 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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 (refl_equal . .)
eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
end of H14
(H15)
consider H14
we proved eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
that is equivalent to eq nat n (r (Bind Abbr) n)
we proceed by induction on the previous result to prove drop (r (Bind Abbr) n) O x (CHead x0 (Bind Abst) u1)
case refl_equal : ⇒
the thesis becomes the hypothesis H12
drop (r (Bind Abbr) n) O x (CHead x0 (Bind Abst) u1)
end of H15
by (drop_drop . . . . H15 .)
we proved drop (S n) O (CHead x (Bind Abbr) t) (CHead x0 (Bind Abst) u1)
by (ex_intro2 . . . . previous H13)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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 : H11:ex4_3 C T A λd2:C.λu2:T.λ:A.drop n O x (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.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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 H11 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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 : x0:C x1:T x2:A H12:drop n O x (CHead x0 (Bind Abbr) x1) H13:csuba g d1 x0 H14:arity g d1 u1 (asucc g x2) H15:arity g x0 x1 x2 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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
(H16)
by (refl_equal . .)
eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
end of H16
(H17)
consider H16
we proved eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
that is equivalent to eq nat n (r (Bind Abbr) n)
we proceed by induction on the previous result to prove drop (r (Bind Abbr) n) O x (CHead x0 (Bind Abbr) x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H12
drop (r (Bind Abbr) n) O x (CHead x0 (Bind Abbr) x1)
end of H17
by (drop_drop . . . . H17 .)
we proved drop (S n) O (CHead x (Bind Abbr) t) (CHead x0 (Bind Abbr) x1)
by (ex4_3_intro . . . . . . . . . . previous H13 H14 H15)
we proved
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abbr) t) (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 (eq_ind_r . . . previous . H8)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
csuba g (CHead c (Bind Abbr) t) c2
→(drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abst) u1)
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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))
suppose H5: csuba g (CHead c (Bind Abst) t) c2
suppose H6: drop (r (Bind Abst) n) O c (CHead d1 (Bind Abst) u1)
(H_x)
by (csuba_gen_abst . . . . H5)
or
ex2 C λd2:C.eq C c2 (CHead d2 (Bind Abst) t) λd2:C.csuba g c d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g c d2
λ:C.λ:T.λa:A.arity g c t (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
end of H_x
(H7) consider H_x
we proceed by induction on H7 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 : H8:ex2 C λd2:C.eq C c2 (CHead d2 (Bind Abst) t) λd2:C.csuba g c d2 ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 H8 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 : x:C H9:eq C c2 (CHead x (Bind Abst) t) H10:csuba g c x ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
(H11)
consider H6
we proved drop (r (Bind Abst) n) O c (CHead d1 (Bind Abst) u1)
that is equivalent to drop n O c (CHead d1 (Bind Abst) u1)
by (H . . . previous . . H10)
or
ex2 C λd2:C.drop n O x (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop n O x (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 H11
we proceed by induction on H11 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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 : H12:ex2 C λd2:C.drop n O x (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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 H12 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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 : x0:C H13:drop n O x (CHead x0 (Bind Abst) u1) H14:csuba g d1 x0 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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
(H15)
by (refl_equal . .)
eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
end of H15
(H16)
consider H15
we proved eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
that is equivalent to eq nat n (r (Bind Abbr) n)
we proceed by induction on the previous result to prove drop (r (Bind Abbr) n) O x (CHead x0 (Bind Abst) u1)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
drop (r (Bind Abbr) n) O x (CHead x0 (Bind Abst) u1)
end of H16
consider H16
we proved drop (r (Bind Abbr) n) O x (CHead x0 (Bind Abst) u1)
that is equivalent to drop (r (Bind Abst) n) O x (CHead x0 (Bind Abst) u1)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x (Bind Abst) t) (CHead x0 (Bind Abst) u1)
by (ex_intro2 . . . . previous H14)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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 : H12:ex4_3 C T A λd2:C.λu2:T.λ:A.drop n O x (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.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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 H12 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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 : x0:C x1:T x2:A H13:drop n O x (CHead x0 (Bind Abbr) x1) H14:csuba g d1 x0 H15:arity g d1 u1 (asucc g x2) H16:arity g x0 x1 x2 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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
(H17)
by (refl_equal . .)
eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
end of H17
(H18)
consider H17
we proved eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
that is equivalent to eq nat n (r (Bind Abbr) n)
we proceed by induction on the previous result to prove drop (r (Bind Abbr) n) O x (CHead x0 (Bind Abbr) x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
drop (r (Bind Abbr) n) O x (CHead x0 (Bind Abbr) x1)
end of H18
consider H18
we proved drop (r (Bind Abbr) n) O x (CHead x0 (Bind Abbr) x1)
that is equivalent to drop (r (Bind Abst) n) O x (CHead x0 (Bind Abbr) x1)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x (Bind Abst) t) (CHead x0 (Bind Abbr) x1)
by (ex4_3_intro . . . . . . . . . . previous H14 H15 H16)
we proved
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C
.λu2:T.λ:A.drop (S n) O (CHead x (Bind Abst) t) (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 (eq_ind_r . . . previous . H9)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 : H8:ex4_3 C T A λd2:C.λu2:T.λ:A.eq C c2 (CHead d2 (Bind Abbr) u2) λd2:C.λ:T.λ:A.csuba g c d2 λ:C.λ:T.λa:A.arity g c t (asucc g a) λd2:C.λu2:T.λa:A.arity g d2 u2 a ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 H8 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 : x0:C x1:T x2:A H9:eq C c2 (CHead x0 (Bind Abbr) x1) H10:csuba g c x0 :arity g c t (asucc g x2) :arity g x0 x1 x2 ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
(H13)
consider H6
we proved drop (r (Bind Abst) n) O c (CHead d1 (Bind Abst) u1)
that is equivalent to drop n O c (CHead d1 (Bind Abst) u1)
by (H . . . previous . . H10)
or
ex2 C λd2:C.drop n O x0 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop n O x0 (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 H13
we proceed by induction on H13 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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 : H14:ex2 C λd2:C.drop n O x0 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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 H14 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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 H15:drop n O x0 (CHead x (Bind Abst) u1) H16:csuba g d1 x ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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
(H17)
by (refl_equal . .)
eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
end of H17
(H18)
consider H17
we proved eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
that is equivalent to eq nat n (r (Bind Abbr) n)
we proceed by induction on the previous result to prove drop (r (Bind Abbr) n) O x0 (CHead x (Bind Abst) u1)
case refl_equal : ⇒
the thesis becomes the hypothesis H15
drop (r (Bind Abbr) n) O x0 (CHead x (Bind Abst) u1)
end of H18
by (drop_drop . . . . H18 .)
we proved drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead x (Bind Abst) u1)
by (ex_intro2 . . . . previous H16)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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 : H14:ex4_3 C T A λd2:C.λu2:T.λ:A.drop n O x0 (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.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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 H14 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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 H15:drop n O x0 (CHead x3 (Bind Abbr) x4) H16:csuba g d1 x3 H17:arity g d1 u1 (asucc g x5) H18:arity g x3 x4 x5 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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
(H19)
by (refl_equal . .)
eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
end of H19
(H20)
consider H19
we proved eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
that is equivalent to eq nat n (r (Bind Abbr) n)
we proceed by induction on the previous result to prove drop (r (Bind Abbr) n) O x0 (CHead x3 (Bind Abbr) x4)
case refl_equal : ⇒
the thesis becomes the hypothesis H15
drop (r (Bind Abbr) n) O x0 (CHead x3 (Bind Abbr) x4)
end of H20
by (drop_drop . . . . H20 .)
we proved drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead x3 (Bind Abbr) x4)
by (ex4_3_intro . . . . . . . . . . previous H16 H17 H18)
we proved
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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.drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Bind Abbr) x1) (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 (eq_ind_r . . . previous . H9)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
csuba g (CHead c (Bind Abst) t) c2
→(drop (r (Bind Abst) n) O c (CHead d1 (Bind Abst) u1)
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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))
suppose H5: csuba g (CHead c (Bind Void) t) c2
suppose H6: drop (r (Bind Void) n) O c (CHead d1 (Bind Abst) u1)
(H_x)
by (csuba_gen_void . . . . H5)
ex2_3 B C T λb:B.λd2:C.λu2:T.eq C c2 (CHead d2 (Bind b) u2) λ:B.λd2:C.λ:T.csuba g c d2
end of H_x
(H7) consider H_x
we proceed by induction on H7 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 ex2_3_intro : x0:B x1:C x2:T H8:eq C c2 (CHead x1 (Bind x0) x2) H9:csuba g c x1 ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
(H10)
consider H6
we proved drop (r (Bind Void) n) O c (CHead d1 (Bind Abst) u1)
that is equivalent to drop n O c (CHead d1 (Bind Abst) u1)
by (H . . . previous . . H9)
or
ex2 C λd2:C.drop n O x1 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop n O x1 (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 H10
we proceed by induction on H10 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
case or_introl : H11:ex2 C λd2:C.drop n O x1 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
we proceed by induction on H11 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
case ex_intro2 : x:C H12:drop n O x1 (CHead x (Bind Abst) u1) H13:csuba g d1 x ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
(H14)
by (refl_equal . .)
eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
end of H14
(H15)
consider H14
we proved eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
that is equivalent to eq nat n (r (Bind Abbr) n)
we proceed by induction on the previous result to prove drop (r (Bind Abbr) n) O x1 (CHead x (Bind Abst) u1)
case refl_equal : ⇒
the thesis becomes the hypothesis H12
drop (r (Bind Abbr) n) O x1 (CHead x (Bind Abst) u1)
end of H15
consider H15
we proved drop (r (Bind Abbr) n) O x1 (CHead x (Bind Abst) u1)
that is equivalent to drop (r (Bind x0) n) O x1 (CHead x (Bind Abst) u1)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x1 (Bind x0) x2) (CHead x (Bind Abst) u1)
by (ex_intro2 . . . . previous H13)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
or
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
case or_intror : H11:ex4_3 C T A λd2:C.λu2:T.λ:A.drop n O x1 (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.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
we proceed by induction on H11 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
case ex4_3_intro : x3:C x4:T x5:A H12:drop n O x1 (CHead x3 (Bind Abbr) x4) H13:csuba g d1 x3 H14:arity g d1 u1 (asucc g x5) H15:arity g x3 x4 x5 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
(H16)
by (refl_equal . .)
eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
end of H16
(H17)
consider H16
we proved eq nat (r (Bind Abbr) n) (r (Bind Abbr) n)
that is equivalent to eq nat n (r (Bind Abbr) n)
we proceed by induction on the previous result to prove drop (r (Bind Abbr) n) O x1 (CHead x3 (Bind Abbr) x4)
case refl_equal : ⇒
the thesis becomes the hypothesis H12
drop (r (Bind Abbr) n) O x1 (CHead x3 (Bind Abbr) x4)
end of H17
consider H17
we proved drop (r (Bind Abbr) n) O x1 (CHead x3 (Bind Abbr) x4)
that is equivalent to drop (r (Bind x0) n) O x1 (CHead x3 (Bind Abbr) x4)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x1 (Bind x0) x2) (CHead x3 (Bind Abbr) x4)
by (ex4_3_intro . . . . . . . . . . previous H13 H14 H15)
we proved
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
by (or_intror . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
or
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
we proved
or
ex2
C
λd2:C.drop (S n) O (CHead x1 (Bind x0) x2) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x1 (Bind x0) 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
by (eq_ind_r . . . previous . H8)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
csuba g (CHead c (Bind Void) t) c2
→(drop (r (Bind Void) n) O c (CHead d1 (Bind Abst) u1)
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 (previous . H3 H4)
we proved
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
∀H3:csuba g (CHead c (Bind b) t) c2
.∀H4:drop (r (Bind b) n) O c (CHead d1 (Bind Abst) u1)
.or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 f: F
suppose H3: csuba g (CHead c (Flat f) t) c2
suppose H4: drop (r (Flat f) n) O c (CHead d1 (Bind Abst) u1)
(H_x)
by (csuba_gen_flat . . . . . H3)
ex2_2 C T λd2:C.λu2:T.eq C c2 (CHead d2 (Flat f) u2) λd2:C.λ:T.csuba g c d2
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 ex2_2_intro : x0:C x1:T H6:eq C c2 (CHead x0 (Flat f) x1) H7:csuba g c x0 ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
(H8)
consider H4
we proved drop (r (Flat f) n) O c (CHead d1 (Bind Abst) u1)
that is equivalent to drop (S n) O c (CHead d1 (Bind Abst) u1)
by (H0 . . previous . . H7)
or
ex2 C λd2:C.drop (S n) O x0 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O x0 (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 H8
we proceed by induction on H8 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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 : H9:ex2 C λd2:C.drop (S n) O x0 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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 H9 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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 H10:drop (S n) O x0 (CHead x (Bind Abst) u1) H11:csuba g d1 x ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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
consider H10
we proved drop (S n) O x0 (CHead x (Bind Abst) u1)
that is equivalent to drop (r (Flat f) n) O x0 (CHead x (Bind Abst) u1)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x0 (Flat f) x1) (CHead x (Bind Abst) u1)
by (ex_intro2 . . . . previous H11)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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 : H9:ex4_3 C T A λd2:C.λu2:T.λ:A.drop (S n) O x0 (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.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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 H9 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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 : x2:C x3:T x4:A H10:drop (S n) O x0 (CHead x2 (Bind Abbr) x3) H11:csuba g d1 x2 H12:arity g d1 u1 (asucc g x4) H13:arity g x2 x3 x4 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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
consider H10
we proved drop (S n) O x0 (CHead x2 (Bind Abbr) x3)
that is equivalent to drop (r (Flat f) n) O x0 (CHead x2 (Bind Abbr) x3)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x0 (Flat f) x1) (CHead x2 (Bind Abbr) x3)
by (ex4_3_intro . . . . . . . . . . previous H11 H12 H13)
we proved
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1)
λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) O (CHead x0 (Flat f) x1) (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 (eq_ind_r . . . previous . H6)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
∀H3:csuba g (CHead c (Flat f) t) c2
.∀H4:drop (r (Flat f) n) O c (CHead d1 (Bind Abst) u1)
.or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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 (previous . H2 previous)
we proved
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
∀d1:C
.∀u1:T
.∀H1:drop (S n) O (CHead c k t) (CHead d1 (Bind Abst) u1)
.∀g:G
.∀c2:C
.∀H2:csuba g (CHead c k t) c2
.or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
∀d1:C
.∀u1:T
.drop (S n) O c1 (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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)
∀c1:C
.∀d1:C
.∀u1:T
.drop (S n) O c1 (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c1 c2
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.drop (S n) 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
∀c1:C
.∀d1:C
.∀u1:T
.drop i O c1 (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c1 c2
→(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)
we proved
∀i:nat
.∀c1:C
.∀d1:C
.∀u1:T
.drop i O c1 (CHead d1 (Bind Abst) u1)
→∀g:G
.∀c2:C
.csuba g c1 c2
→(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)