DEFINITION ty3_ind()
TYPE =
∀g:G
.∀P:C→T→T→Prop
.∀c:C
.∀t:T
.∀t1:T
.ty3 g c t t1
→(P c t t1)→∀t2:T.∀t3:T.(ty3 g c t2 t3)→(P c t2 t3)→(pc3 c t3 t)→(P c t2 t)
→(∀c:C.∀n:nat.(P c (TSort n) (TSort (next g n)))
→(∀n:nat
.∀c:C
.∀c1:C
.∀t:T
.getl n c (CHead c1 (Bind Abbr) t)
→∀t1:T.(ty3 g c1 t t1)→(P c1 t t1)→(P c (TLRef n) (lift (S n) O t1))
→(∀n:nat
.∀c:C
.∀c1:C
.∀t:T
.getl n c (CHead c1 (Bind Abst) t)
→∀t1:T.(ty3 g c1 t t1)→(P c1 t t1)→(P c (TLRef n) (lift (S n) O t))
→(∀c:C
.∀t:T
.∀t1:T
.ty3 g c t t1
→(P c t t1
→∀b:B
.∀t2:T
.∀t3:T
.ty3 g (CHead c (Bind b) t) t2 t3
→(P (CHead c (Bind b) t) t2 t3
→P c (THead (Bind b) t t2) (THead (Bind b) t t3)))
→(∀c:C
.∀t:T
.∀t1:T
.ty3 g c t t1
→(P c t t1
→∀t2:T
.∀t3:T
.ty3 g c t2 (THead (Bind Abst) t1 t3)
→(P c t2 (THead (Bind Abst) t1 t3)
→(P
c
THead (Flat Appl) t t2
THead (Flat Appl) t (THead (Bind Abst) t1 t3))))
→(∀c:C
.∀t:T
.∀t1:T
.ty3 g c t t1
→(P c t t1
→∀t2:T
.ty3 g c t1 t2
→(P c t1 t2)→(P c (THead (Flat Cast) t1 t) (THead (Flat Cast) t2 t1)))
→∀c:C.∀t:T.∀t1:T.(ty3 g c t t1)→(P c t t1)))))))
BODY =
Show proof