DEFINITION csuba_ind()
TYPE =
∀g:G
.∀P:C→C→Prop
.∀n:nat.(P (CSort n) (CSort n))
→(∀c:C
.∀c1:C.(csuba g c c1)→(P c c1)→∀k:K.∀t:T.(P (CHead c k t) (CHead c1 k t))
→(∀c:C
.∀c1:C
.csuba g c c1
→(P c c1
→∀b:B
.not (eq B b Void)
→∀t:T.∀t1:T.(P (CHead c (Bind Void) t) (CHead c1 (Bind b) t1)))
→(∀c:C
.∀c1:C
.csuba g c c1
→(P c c1
→∀t:T
.∀a:A
.arity g c t (asucc g a)
→∀t1:T
.arity g c1 t1 a
→P (CHead c (Bind Abst) t) (CHead c1 (Bind Abbr) t1))
→∀c:C.∀c1:C.(csuba g c c1)→(P c c1))))
BODY =
Show proof