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 =
assume g: G
assume P: C→T→T→Prop
suppose H:
∀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)
suppose H1: ∀c:C.∀n:nat.(P c (TSort n) (TSort (next g n)))
suppose H2:
∀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))
suppose H3:
∀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))
suppose H4:
∀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)))
suppose H5:
∀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))))
suppose H6:
∀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)))
(aux) by well-founded reasoning we prove ∀c:C.∀t:T.∀t1:T.(ty3 g c t t1)→(P c t t1)
assume c: C
assume t: T
assume t1: T
suppose H7: ty3 g c t t1
by cases on H7 we prove P c t t1
case ty3_conv c1:C t2:T t3:T H8:ty3 g c1 t2 t3 t4:T t5:T H9:ty3 g c1 t4 t5 H10:pc3 c1 t5 t2 ⇒
the thesis becomes P c1 t4 t2
(h1) by (aux . . . H8) we proved P c1 t2 t3
(h2) by (aux . . . H9) we proved P c1 t4 t5
by (H . . . H8 h1 . . H9 h2 H10)
P c1 t4 t2
case ty3_sort c1:C n:nat ⇒
the thesis becomes P c1 (TSort n) (TSort (next g n))
by (H1 . .)
P c1 (TSort n) (TSort (next g n))
case ty3_abbr n:nat c1:C c2:C t2:T H8:getl n c1 (CHead c2 (Bind Abbr) t2) t3:T H9:ty3 g c2 t2 t3 ⇒
the thesis becomes P c1 (TLRef n) (lift (S n) O t3)
by (aux . . . H9)
we proved P c2 t2 t3
by (H2 . . . . H8 . H9 previous)
P c1 (TLRef n) (lift (S n) O t3)
case ty3_abst n:nat c1:C c2:C t2:T H8:getl n c1 (CHead c2 (Bind Abst) t2) t3:T H9:ty3 g c2 t2 t3 ⇒
the thesis becomes P c1 (TLRef n) (lift (S n) O t2)
by (aux . . . H9)
we proved P c2 t2 t3
by (H3 . . . . H8 . H9 previous)
P c1 (TLRef n) (lift (S n) O t2)
case ty3_bind c1:C t2:T t3:T H8:ty3 g c1 t2 t3 b:B t4:T t5:T H9:ty3 g (CHead c1 (Bind b) t2) t4 t5 ⇒
the thesis becomes P c1 (THead (Bind b) t2 t4) (THead (Bind b) t2 t5)
(h1) by (aux . . . H8) we proved P c1 t2 t3
(h2)
by (aux . . . H9)
P (CHead c1 (Bind b) t2) t4 t5
end of h2
by (H4 . . . H8 h1 . . . H9 h2)
P c1 (THead (Bind b) t2 t4) (THead (Bind b) t2 t5)
case ty3_appl c1:C t2:T t3:T H8:ty3 g c1 t2 t3 t4:T t5:T H9:ty3 g c1 t4 (THead (Bind Abst) t3 t5) ⇒
the thesis becomes
P
c1
THead (Flat Appl) t2 t4
THead (Flat Appl) t2 (THead (Bind Abst) t3 t5)
(h1) by (aux . . . H8) we proved P c1 t2 t3
(h2)
by (aux . . . H9)
P c1 t4 (THead (Bind Abst) t3 t5)
end of h2
by (H5 . . . H8 h1 . . H9 h2)
P
c1
THead (Flat Appl) t2 t4
THead (Flat Appl) t2 (THead (Bind Abst) t3 t5)
case ty3_cast c1:C t2:T t3:T H8:ty3 g c1 t2 t3 t4:T H9:ty3 g c1 t3 t4 ⇒
the thesis becomes P c1 (THead (Flat Cast) t3 t2) (THead (Flat Cast) t4 t3)
(h1) by (aux . . . H8) we proved P c1 t2 t3
(h2) by (aux . . . H9) we proved P c1 t3 t4
by (H6 . . . H8 h1 . H9 h2)
P c1 (THead (Flat Cast) t3 t2) (THead (Flat Cast) t4 t3)
we proved P c t t1
∀c:C.∀t:T.∀t1:T.(ty3 g c t t1)→(P c t t1)
done
consider aux
we proved ∀c:C.∀t:T.∀t1:T.(ty3 g c t t1)→(P c t t1)
we proved
∀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)))))))