DEFINITION arity_ind()
TYPE =
∀g:G
.∀P:C→T→A→Prop
.∀c:C.∀n:nat.(P c (TSort n) (ASort O n))
→(∀c:C
.∀c1:C
.∀t:T
.∀n:nat
.getl n c (CHead c1 (Bind Abbr) t)
→∀a:A.(arity g c1 t a)→(P c1 t a)→(P c (TLRef n) a)
→(∀c:C
.∀c1:C
.∀t:T
.∀n:nat
.getl n c (CHead c1 (Bind Abst) t)
→∀a:A
.arity g c1 t (asucc g a)
→(P c1 t (asucc g a))→(P c (TLRef n) a)
→(∀b:B
.not (eq B b Abst)
→∀c:C
.∀t:T
.∀a:A
.arity g c t a
→(P c t a
→∀t1:T
.∀a1:A
.arity g (CHead c (Bind b) t) t1 a1
→(P (CHead c (Bind b) t) t1 a1)→(P c (THead (Bind b) t t1) a1))
→(∀c:C
.∀t:T
.∀a:A
.arity g c t (asucc g a)
→(P c t (asucc g a)
→∀t1:T
.∀a1:A
.arity g (CHead c (Bind Abst) t) t1 a1
→(P (CHead c (Bind Abst) t) t1 a1
→P c (THead (Bind Abst) t t1) (AHead a a1)))
→(∀c:C
.∀t:T
.∀a:A
.arity g c t a
→(P c t a
→∀t1:T
.∀a1:A
.arity g c t1 (AHead a a1)
→(P c t1 (AHead a a1))→(P c (THead (Flat Appl) t t1) a1))
→(∀c:C
.∀t:T
.∀a:A
.arity g c t (asucc g a)
→(P c t (asucc g a)
→∀t1:T.(arity g c t1 a)→(P c t1 a)→(P c (THead (Flat Cast) t t1) a))
→(∀c:C.∀t:T.∀a:A.(arity g c t a)→(P c t a)→∀a1:A.(leq g a a1)→(P c t a1)
→∀c:C.∀t:T.∀a:A.(arity g c t a)→(P c t a))))))))
BODY =
assume g: G
assume P: C→T→A→Prop
suppose H: ∀c:C.∀n:nat.(P c (TSort n) (ASort O n))
suppose H1:
∀c:C
.∀c1:C
.∀t:T
.∀n:nat
.getl n c (CHead c1 (Bind Abbr) t)
→∀a:A.(arity g c1 t a)→(P c1 t a)→(P c (TLRef n) a)
suppose H2:
∀c:C
.∀c1:C
.∀t:T
.∀n:nat
.getl n c (CHead c1 (Bind Abst) t)
→∀a:A
.arity g c1 t (asucc g a)
→(P c1 t (asucc g a))→(P c (TLRef n) a)
suppose H3:
∀b:B
.not (eq B b Abst)
→∀c:C
.∀t:T
.∀a:A
.arity g c t a
→(P c t a
→∀t1:T
.∀a1:A
.arity g (CHead c (Bind b) t) t1 a1
→(P (CHead c (Bind b) t) t1 a1)→(P c (THead (Bind b) t t1) a1))
suppose H4:
∀c:C
.∀t:T
.∀a:A
.arity g c t (asucc g a)
→(P c t (asucc g a)
→∀t1:T
.∀a1:A
.arity g (CHead c (Bind Abst) t) t1 a1
→(P (CHead c (Bind Abst) t) t1 a1
→P c (THead (Bind Abst) t t1) (AHead a a1)))
suppose H5:
∀c:C
.∀t:T
.∀a:A
.arity g c t a
→(P c t a
→∀t1:T
.∀a1:A
.arity g c t1 (AHead a a1)
→(P c t1 (AHead a a1))→(P c (THead (Flat Appl) t t1) a1))
suppose H6:
∀c:C
.∀t:T
.∀a:A
.arity g c t (asucc g a)
→(P c t (asucc g a)
→∀t1:T.(arity g c t1 a)→(P c t1 a)→(P c (THead (Flat Cast) t t1) a))
suppose H7:
∀c:C.∀t:T.∀a:A.(arity g c t a)→(P c t a)→∀a1:A.(leq g a a1)→(P c t a1)
(aux) by well-founded reasoning we prove ∀c:C.∀t:T.∀a:A.(arity g c t a)→(P c t a)
assume c: C
assume t: T
assume a: A
suppose H8: arity g c t a
by cases on H8 we prove P c t a
case arity_sort c1:C n:nat ⇒
the thesis becomes P c1 (TSort n) (ASort O n)
by (H . .)
P c1 (TSort n) (ASort O n)
case arity_abbr c1:C c2:C t1:T n:nat H9:getl n c1 (CHead c2 (Bind Abbr) t1) a1:A H10:arity g c2 t1 a1 ⇒
the thesis becomes P c1 (TLRef n) a1
by (aux . . . H10)
we proved P c2 t1 a1
by (H1 . . . . H9 . H10 previous)
P c1 (TLRef n) a1
case arity_abst c1:C c2:C t1:T n:nat H9:getl n c1 (CHead c2 (Bind Abst) t1) a1:A H10:arity g c2 t1 (asucc g a1) ⇒
the thesis becomes P c1 (TLRef n) a1
by (aux . . . H10)
we proved P c2 t1 (asucc g a1)
by (H2 . . . . H9 . H10 previous)
P c1 (TLRef n) a1
case arity_bind b:B H9:not (eq B b Abst) c1:C t1:T a1:A H10:arity g c1 t1 a1 t2:T a2:A H11:arity g (CHead c1 (Bind b) t1) t2 a2 ⇒
the thesis becomes P c1 (THead (Bind b) t1 t2) a2
(h1) by (aux . . . H10) we proved P c1 t1 a1
(h2)
by (aux . . . H11)
P (CHead c1 (Bind b) t1) t2 a2
end of h2
by (H3 . H9 . . . H10 h1 . . H11 h2)
P c1 (THead (Bind b) t1 t2) a2
case arity_head c1:C t1:T a1:A H9:arity g c1 t1 (asucc g a1) t2:T a2:A H10:arity g (CHead c1 (Bind Abst) t1) t2 a2 ⇒
the thesis becomes P c1 (THead (Bind Abst) t1 t2) (AHead a1 a2)
(h1)
by (aux . . . H9)
P c1 t1 (asucc g a1)
end of h1
(h2)
by (aux . . . H10)
P (CHead c1 (Bind Abst) t1) t2 a2
end of h2
by (H4 . . . H9 h1 . . H10 h2)
P c1 (THead (Bind Abst) t1 t2) (AHead a1 a2)
case arity_appl c1:C t1:T a1:A H9:arity g c1 t1 a1 t2:T a2:A H10:arity g c1 t2 (AHead a1 a2) ⇒
the thesis becomes P c1 (THead (Flat Appl) t1 t2) a2
(h1) by (aux . . . H9) we proved P c1 t1 a1
(h2)
by (aux . . . H10)
P c1 t2 (AHead a1 a2)
end of h2
by (H5 . . . H9 h1 . . H10 h2)
P c1 (THead (Flat Appl) t1 t2) a2
case arity_cast c1:C t1:T a1:A H9:arity g c1 t1 (asucc g a1) t2:T H10:arity g c1 t2 a1 ⇒
the thesis becomes P c1 (THead (Flat Cast) t1 t2) a1
(h1)
by (aux . . . H9)
P c1 t1 (asucc g a1)
end of h1
(h2) by (aux . . . H10) we proved P c1 t2 a1
by (H6 . . . H9 h1 . H10 h2)
P c1 (THead (Flat Cast) t1 t2) a1
case arity_repl c1:C t1:T a1:A H9:arity g c1 t1 a1 a2:A H10:leq g a1 a2 ⇒
the thesis becomes P c1 t1 a2
by (aux . . . H9)
we proved P c1 t1 a1
by (H7 . . . H9 previous . H10)
P c1 t1 a2
we proved P c t a
∀c:C.∀t:T.∀a:A.(arity g c t a)→(P c t a)
done
consider aux
we proved ∀c:C.∀t:T.∀a:A.(arity g c t a)→(P c t a)
we proved
∀g:G
.∀P:C→T→A→Prop
.∀c:C.∀n:nat.(P c (TSort n) (ASort O n))
→(∀c:C
.∀c1:C
.∀t:T
.∀n:nat
.getl n c (CHead c1 (Bind Abbr) t)
→∀a:A.(arity g c1 t a)→(P c1 t a)→(P c (TLRef n) a)
→(∀c:C
.∀c1:C
.∀t:T
.∀n:nat
.getl n c (CHead c1 (Bind Abst) t)
→∀a:A
.arity g c1 t (asucc g a)
→(P c1 t (asucc g a))→(P c (TLRef n) a)
→(∀b:B
.not (eq B b Abst)
→∀c:C
.∀t:T
.∀a:A
.arity g c t a
→(P c t a
→∀t1:T
.∀a1:A
.arity g (CHead c (Bind b) t) t1 a1
→(P (CHead c (Bind b) t) t1 a1)→(P c (THead (Bind b) t t1) a1))
→(∀c:C
.∀t:T
.∀a:A
.arity g c t (asucc g a)
→(P c t (asucc g a)
→∀t1:T
.∀a1:A
.arity g (CHead c (Bind Abst) t) t1 a1
→(P (CHead c (Bind Abst) t) t1 a1
→P c (THead (Bind Abst) t t1) (AHead a a1)))
→(∀c:C
.∀t:T
.∀a:A
.arity g c t a
→(P c t a
→∀t1:T
.∀a1:A
.arity g c t1 (AHead a a1)
→(P c t1 (AHead a a1))→(P c (THead (Flat Appl) t t1) a1))
→(∀c:C
.∀t:T
.∀a:A
.arity g c t (asucc g a)
→(P c t (asucc g a)
→∀t1:T.(arity g c t1 a)→(P c t1 a)→(P c (THead (Flat Cast) t t1) a))
→(∀c:C.∀t:T.∀a:A.(arity g c t a)→(P c t a)→∀a1:A.(leq g a a1)→(P c t a1)
→∀c:C.∀t:T.∀a:A.(arity g c t a)→(P c t a))))))))