DEFINITION pr0_ind()
TYPE =
∀P:T→T→Prop
.∀t:T.(P t t)
→(∀t:T
.∀t1:T
.pr0 t t1
→(P t t1)→∀t2:T.∀t3:T.(pr0 t2 t3)→(P t2 t3)→∀k:K.(P (THead k t t2) (THead k t1 t3))
→(∀t:T
.∀t1:T
.∀t2:T
.pr0 t1 t2
→(P t1 t2
→∀t3:T
.∀t4:T
.pr0 t3 t4
→(P t3 t4
→(P
THead (Flat Appl) t1 (THead (Bind Abst) t t3)
THead (Bind Abbr) t2 t4)))
→(∀b:B
.not (eq B b Abst)
→∀t:T
.∀t1:T
.pr0 t t1
→(P t t1
→∀t2:T
.∀t3:T
.pr0 t2 t3
→(P t2 t3
→∀t4:T
.∀t5:T
.pr0 t4 t5
→(P t4 t5
→(P
THead (Flat Appl) t (THead (Bind b) t2 t4)
THead (Bind b) t3 (THead (Flat Appl) (lift (S O) O t1) t5)))))
→(∀t:T
.∀t1:T
.pr0 t t1
→(P t t1
→∀t2:T
.∀t3:T
.pr0 t2 t3
→(P t2 t3
→∀t4:T.(subst0 O t1 t3 t4)→(P (THead (Bind Abbr) t t2) (THead (Bind Abbr) t1 t4))))
→(∀b:B
.not (eq B b Abst)
→∀t:T
.∀t1:T.(pr0 t t1)→(P t t1)→∀t2:T.(P (THead (Bind b) t2 (lift (S O) O t)) t1)
→(∀t:T.∀t1:T.(pr0 t t1)→(P t t1)→∀t2:T.(P (THead (Flat Cast) t2 t) t1)
→∀t:T.∀t1:T.(pr0 t t1)→(P t t1)))))))
BODY =
assume P: T→T→Prop
suppose H: ∀t:T.(P t t)
suppose H1:
∀t:T
.∀t1:T
.pr0 t t1
→(P t t1)→∀t2:T.∀t3:T.(pr0 t2 t3)→(P t2 t3)→∀k:K.(P (THead k t t2) (THead k t1 t3))
suppose H2:
∀t:T
.∀t1:T
.∀t2:T
.pr0 t1 t2
→(P t1 t2
→∀t3:T
.∀t4:T
.pr0 t3 t4
→(P t3 t4
→(P
THead (Flat Appl) t1 (THead (Bind Abst) t t3)
THead (Bind Abbr) t2 t4)))
suppose H3:
∀b:B
.not (eq B b Abst)
→∀t:T
.∀t1:T
.pr0 t t1
→(P t t1
→∀t2:T
.∀t3:T
.pr0 t2 t3
→(P t2 t3
→∀t4:T
.∀t5:T
.pr0 t4 t5
→(P t4 t5
→(P
THead (Flat Appl) t (THead (Bind b) t2 t4)
THead (Bind b) t3 (THead (Flat Appl) (lift (S O) O t1) t5)))))
suppose H4:
∀t:T
.∀t1:T
.pr0 t t1
→(P t t1
→∀t2:T
.∀t3:T
.pr0 t2 t3
→(P t2 t3
→∀t4:T.(subst0 O t1 t3 t4)→(P (THead (Bind Abbr) t t2) (THead (Bind Abbr) t1 t4))))
suppose H5:
∀b:B
.not (eq B b Abst)
→∀t:T
.∀t1:T.(pr0 t t1)→(P t t1)→∀t2:T.(P (THead (Bind b) t2 (lift (S O) O t)) t1)
suppose H6: ∀t:T.∀t1:T.(pr0 t t1)→(P t t1)→∀t2:T.(P (THead (Flat Cast) t2 t) t1)
(aux) by well-founded reasoning we prove ∀t:T.∀t1:T.(pr0 t t1)→(P t t1)
assume t: T
assume t1: T
suppose H7: pr0 t t1
by cases on H7 we prove P t t1
case pr0_refl t2:T ⇒
the thesis becomes P t2 t2
by (H .)
P t2 t2
case pr0_comp t2:T t3:T H8:pr0 t2 t3 t4:T t5:T H9:pr0 t4 t5 k:K ⇒
the thesis becomes P (THead k t2 t4) (THead k t3 t5)
(h1) by (aux . . H8) we proved P t2 t3
(h2) by (aux . . H9) we proved P t4 t5
by (H1 . . H8 h1 . . H9 h2 .)
P (THead k t2 t4) (THead k t3 t5)
case pr0_beta t2:T t3:T t4:T H8:pr0 t3 t4 t5:T t6:T H9:pr0 t5 t6 ⇒
the thesis becomes
P
THead (Flat Appl) t3 (THead (Bind Abst) t2 t5)
THead (Bind Abbr) t4 t6
(h1) by (aux . . H8) we proved P t3 t4
(h2) by (aux . . H9) we proved P t5 t6
by (H2 . . . H8 h1 . . H9 h2)
P
THead (Flat Appl) t3 (THead (Bind Abst) t2 t5)
THead (Bind Abbr) t4 t6
case pr0_upsilon b:B H8:not (eq B b Abst) t2:T t3:T H9:pr0 t2 t3 t4:T t5:T H10:pr0 t4 t5 t6:T t7:T H11:pr0 t6 t7 ⇒
the thesis becomes
P
THead (Flat Appl) t2 (THead (Bind b) t4 t6)
THead (Bind b) t5 (THead (Flat Appl) (lift (S O) O t3) t7)
(h1) by (aux . . H9) we proved P t2 t3
(h2) by (aux . . H10) we proved P t4 t5
(h3) by (aux . . H11) we proved P t6 t7
by (H3 . H8 . . H9 h1 . . H10 h2 . . H11 h3)
P
THead (Flat Appl) t2 (THead (Bind b) t4 t6)
THead (Bind b) t5 (THead (Flat Appl) (lift (S O) O t3) t7)
case pr0_delta t2:T t3:T H8:pr0 t2 t3 t4:T t5:T H9:pr0 t4 t5 t6:T H10:subst0 O t3 t5 t6 ⇒
the thesis becomes P (THead (Bind Abbr) t2 t4) (THead (Bind Abbr) t3 t6)
(h1) by (aux . . H8) we proved P t2 t3
(h2) by (aux . . H9) we proved P t4 t5
by (H4 . . H8 h1 . . H9 h2 . H10)
P (THead (Bind Abbr) t2 t4) (THead (Bind Abbr) t3 t6)
case pr0_zeta b:B H8:not (eq B b Abst) t2:T t3:T H9:pr0 t2 t3 t4:T ⇒
the thesis becomes P (THead (Bind b) t4 (lift (S O) O t2)) t3
by (aux . . H9)
we proved P t2 t3
by (H5 . H8 . . H9 previous .)
P (THead (Bind b) t4 (lift (S O) O t2)) t3
case pr0_tau t2:T t3:T H8:pr0 t2 t3 t4:T ⇒
the thesis becomes P (THead (Flat Cast) t4 t2) t3
by (aux . . H8)
we proved P t2 t3
by (H6 . . H8 previous .)
P (THead (Flat Cast) t4 t2) t3
we proved P t t1
∀t:T.∀t1:T.(pr0 t t1)→(P t t1)
done
consider aux
we proved ∀t:T.∀t1:T.(pr0 t t1)→(P t t1)
we proved
∀P:T→T→Prop
.∀t:T.(P t t)
→(∀t:T
.∀t1:T
.pr0 t t1
→(P t t1)→∀t2:T.∀t3:T.(pr0 t2 t3)→(P t2 t3)→∀k:K.(P (THead k t t2) (THead k t1 t3))
→(∀t:T
.∀t1:T
.∀t2:T
.pr0 t1 t2
→(P t1 t2
→∀t3:T
.∀t4:T
.pr0 t3 t4
→(P t3 t4
→(P
THead (Flat Appl) t1 (THead (Bind Abst) t t3)
THead (Bind Abbr) t2 t4)))
→(∀b:B
.not (eq B b Abst)
→∀t:T
.∀t1:T
.pr0 t t1
→(P t t1
→∀t2:T
.∀t3:T
.pr0 t2 t3
→(P t2 t3
→∀t4:T
.∀t5:T
.pr0 t4 t5
→(P t4 t5
→(P
THead (Flat Appl) t (THead (Bind b) t2 t4)
THead (Bind b) t3 (THead (Flat Appl) (lift (S O) O t1) t5)))))
→(∀t:T
.∀t1:T
.pr0 t t1
→(P t t1
→∀t2:T
.∀t3:T
.pr0 t2 t3
→(P t2 t3
→∀t4:T.(subst0 O t1 t3 t4)→(P (THead (Bind Abbr) t t2) (THead (Bind Abbr) t1 t4))))
→(∀b:B
.not (eq B b Abst)
→∀t:T
.∀t1:T.(pr0 t t1)→(P t t1)→∀t2:T.(P (THead (Bind b) t2 (lift (S O) O t)) t1)
→(∀t:T.∀t1:T.(pr0 t t1)→(P t t1)→∀t2:T.(P (THead (Flat Cast) t2 t) t1)
→∀t:T.∀t1:T.(pr0 t t1)→(P t t1)))))))