DEFINITION pr1_strip()
TYPE =
∀t0:T.∀t1:T.(pr1 t0 t1)→∀t2:T.(pr0 t0 t2)→(ex2 T λt:T.pr1 t1 t λt:T.pr1 t2 t)
BODY =
assume t0: T
assume t1: T
suppose H: pr1 t0 t1
we proceed by induction on H to prove ∀t3:T.(pr0 t0 t3)→(ex2 T λt4:T.pr1 t1 t4 λt4:T.pr1 t3 t4)
case pr1_refl : t:T ⇒
the thesis becomes ∀t2:T.∀H0:(pr0 t t2).(ex2 T λt3:T.pr1 t t3 λt3:T.pr1 t2 t3)
assume t2: T
suppose H0: pr0 t t2
(h1) by (pr1_pr0 . . H0) we proved pr1 t t2
(h2) by (pr1_refl .) we proved pr1 t2 t2
by (ex_intro2 . . . . h1 h2)
we proved ex2 T λt3:T.pr1 t t3 λt3:T.pr1 t2 t3
∀t2:T.∀H0:(pr0 t t2).(ex2 T λt3:T.pr1 t t3 λt3:T.pr1 t2 t3)
case pr1_sing : t2:T t3:T H0:pr0 t3 t2 t4:T :pr1 t2 t4 ⇒
the thesis becomes ∀t5:T.∀H3:(pr0 t3 t5).(ex2 T λt:T.pr1 t4 t λt:T.pr1 t5 t)
(H2) by induction hypothesis we know ∀t5:T.(pr0 t2 t5)→(ex2 T λt:T.pr1 t4 t λt:T.pr1 t5 t)
assume t5: T
suppose H3: pr0 t3 t5
by (pr0_confluence . . H3 . H0)
we proved ex2 T λt:T.pr0 t5 t λt:T.pr0 t2 t
we proceed by induction on the previous result to prove ex2 T λt:T.pr1 t4 t λt:T.pr1 t5 t
case ex_intro2 : x:T H4:pr0 t5 x H5:pr0 t2 x ⇒
the thesis becomes ex2 T λt:T.pr1 t4 t λt:T.pr1 t5 t
(H6)
by (H2 . H5)
ex2 T λt:T.pr1 t4 t λt:T.pr1 x t
end of H6
we proceed by induction on H6 to prove ex2 T λt:T.pr1 t4 t λt:T.pr1 t5 t
case ex_intro2 : x0:T H7:pr1 t4 x0 H8:pr1 x x0 ⇒
the thesis becomes ex2 T λt:T.pr1 t4 t λt:T.pr1 t5 t
by (pr1_pr0 . . H4)
we proved pr1 t5 x
by (pr1_t . . previous . H8)
we proved pr1 t5 x0
by (ex_intro2 . . . . H7 previous)
ex2 T λt:T.pr1 t4 t λt:T.pr1 t5 t
ex2 T λt:T.pr1 t4 t λt:T.pr1 t5 t
we proved ex2 T λt:T.pr1 t4 t λt:T.pr1 t5 t
∀t5:T.∀H3:(pr0 t3 t5).(ex2 T λt:T.pr1 t4 t λt:T.pr1 t5 t)
we proved ∀t3:T.(pr0 t0 t3)→(ex2 T λt4:T.pr1 t1 t4 λt4:T.pr1 t3 t4)
we proved ∀t0:T.∀t1:T.(pr1 t0 t1)→∀t3:T.(pr0 t0 t3)→(ex2 T λt4:T.pr1 t1 t4 λt4:T.pr1 t3 t4)