DEFINITION tys3_ind()
TYPE =
∀g:G
.∀c:C
.∀P:TList→T→Prop
.∀t:T.∀t1:T.(ty3 g c t t1)→(P TNil t)
→(∀t:T.∀t1:T.(ty3 g c t t1)→∀t2:TList.(tys3 g c t2 t1)→(P t2 t1)→(P (TCons t t2) t1)
→∀t:TList.∀t1:T.(tys3 g c t t1)→(P t t1))
BODY =
assume g: G
assume c: C
assume P: TList→T→Prop
suppose H: ∀t:T.∀t1:T.(ty3 g c t t1)→(P TNil t)
suppose H1: ∀t:T.∀t1:T.(ty3 g c t t1)→∀t2:TList.(tys3 g c t2 t1)→(P t2 t1)→(P (TCons t t2) t1)
(aux) by well-founded reasoning we prove ∀t:TList.∀t1:T.(tys3 g c t t1)→(P t t1)
assume t: TList
assume t1: T
suppose H2: tys3 g c t t1
by cases on H2 we prove P t t1
case tys3_nil t2:T t3:T H3:ty3 g c t2 t3 ⇒
the thesis becomes P TNil t2
by (H . . H3)
P TNil t2
case tys3_cons t2:T t3:T H3:ty3 g c t2 t3 t4:TList H4:tys3 g c t4 t3 ⇒
the thesis becomes P (TCons t2 t4) t3
by (aux . . H4)
we proved P t4 t3
by (H1 . . H3 . H4 previous)
P (TCons t2 t4) t3
we proved P t t1
∀t:TList.∀t1:T.(tys3 g c t t1)→(P t t1)
done
consider aux
we proved ∀t:TList.∀t1:T.(tys3 g c t t1)→(P t t1)
we proved
∀g:G
.∀c:C
.∀P:TList→T→Prop
.∀t:T.∀t1:T.(ty3 g c t t1)→(P TNil t)
→(∀t:T.∀t1:T.(ty3 g c t t1)→∀t2:TList.(tys3 g c t2 t1)→(P t2 t1)→(P (TCons t t2) t1)
→∀t:TList.∀t1:T.(tys3 g c t t1)→(P t t1))