DEFINITION drop1_gen_pcons()
TYPE =
∀c1:C
.∀c3:C
.∀hds:PList
.∀h:nat.∀d:nat.(drop1 (PCons h d hds) c1 c3)→(ex2 C λc2:C.drop h d c1 c2 λc2:C.drop1 hds c2 c3)
BODY =
assume c1: C
assume c3: C
assume hds: PList
assume h: nat
assume d: nat
suppose H: drop1 (PCons h d hds) c1 c3
assume y: PList
suppose H0: drop1 y c1 c3
we proceed by induction on H0 to prove (eq PList y (PCons h d hds))→(ex2 C λc2:C.drop h d c1 c2 λc2:C.drop1 hds c2 c3)
case drop1_nil : c:C ⇒
the thesis becomes ∀H1:(eq PList PNil (PCons h d hds)).(ex2 C λc2:C.drop h d c c2 λc2:C.drop1 hds c2 c)
suppose H1: eq PList PNil (PCons h d hds)
(H2)
we proceed by induction on H1 to prove <λ:PList.Prop> CASE PCons h d hds OF PNil⇒True | PCons ⇒False
case refl_equal : ⇒
the thesis becomes <λ:PList.Prop> CASE PNil OF PNil⇒True | PCons ⇒False
consider I
we proved True
<λ:PList.Prop> CASE PNil OF PNil⇒True | PCons ⇒False
<λ:PList.Prop> CASE PCons h d hds OF PNil⇒True | PCons ⇒False
end of H2
consider H2
we proved <λ:PList.Prop> CASE PCons h d hds OF PNil⇒True | PCons ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove ex2 C λc2:C.drop h d c c2 λc2:C.drop1 hds c2 c
we proved ex2 C λc2:C.drop h d c c2 λc2:C.drop1 hds c2 c
∀H1:(eq PList PNil (PCons h d hds)).(ex2 C λc2:C.drop h d c c2 λc2:C.drop1 hds c2 c)
case drop1_cons : c2:C c4:C h0:nat d0:nat H1:drop h0 d0 c2 c4 c5:C hds0:PList H2:drop1 hds0 c4 c5 ⇒
the thesis becomes ∀H4:(eq PList (PCons h0 d0 hds0) (PCons h d hds)).(ex2 C λc6:C.drop h d c2 c6 λc6:C.drop1 hds c6 c5)
(H3) by induction hypothesis we know (eq PList hds0 (PCons h d hds))→(ex2 C λc6:C.drop h d c4 c6 λc6:C.drop1 hds c6 c5)
suppose H4: eq PList (PCons h0 d0 hds0) (PCons h d hds)
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:PList.nat> CASE PCons h0 d0 hds0 OF PNil⇒h0 | PCons n ⇒n
<λ:PList.nat> CASE PCons h d hds OF PNil⇒h0 | PCons n ⇒n
eq
nat
λe:PList.<λ:PList.nat> CASE e OF PNil⇒h0 | PCons n ⇒n (PCons h0 d0 hds0)
λe:PList.<λ:PList.nat> CASE e OF PNil⇒h0 | PCons n ⇒n (PCons h d hds)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:PList.nat> CASE PCons h0 d0 hds0 OF PNil⇒d0 | PCons n ⇒n
<λ:PList.nat> CASE PCons h d hds OF PNil⇒d0 | PCons n ⇒n
eq
nat
λe:PList.<λ:PList.nat> CASE e OF PNil⇒d0 | PCons n ⇒n (PCons h0 d0 hds0)
λe:PList.<λ:PList.nat> CASE e OF PNil⇒d0 | PCons n ⇒n (PCons h d hds)
end of H6
(h1)
(H7)
by (f_equal . . . . . H4)
we proved
eq
PList
<λ:PList.PList> CASE PCons h0 d0 hds0 OF PNil⇒hds0 | PCons p⇒p
<λ:PList.PList> CASE PCons h d hds OF PNil⇒hds0 | PCons p⇒p
eq
PList
λe:PList.<λ:PList.PList> CASE e OF PNil⇒hds0 | PCons p⇒p (PCons h0 d0 hds0)
λe:PList.<λ:PList.PList> CASE e OF PNil⇒hds0 | PCons p⇒p (PCons h d hds)
end of H7
suppose H8: eq nat d0 d
suppose H9: eq nat h0 h
(H11)
consider H7
we proved
eq
PList
<λ:PList.PList> CASE PCons h0 d0 hds0 OF PNil⇒hds0 | PCons p⇒p
<λ:PList.PList> CASE PCons h d hds OF PNil⇒hds0 | PCons p⇒p
that is equivalent to eq PList hds0 hds
we proceed by induction on the previous result to prove drop1 hds c4 c5
case refl_equal : ⇒
the thesis becomes the hypothesis H2
drop1 hds c4 c5
end of H11
(H12)
we proceed by induction on H8 to prove drop h0 d c2 c4
case refl_equal : ⇒
the thesis becomes the hypothesis H1
drop h0 d c2 c4
end of H12
(H13)
we proceed by induction on H9 to prove drop h d c2 c4
case refl_equal : ⇒
the thesis becomes the hypothesis H12
drop h d c2 c4
end of H13
by (ex_intro2 . . . . H13 H11)
we proved ex2 C λc6:C.drop h d c2 c6 λc6:C.drop1 hds c6 c5
(eq nat d0 d)→(eq nat h0 h)→(ex2 C λc6:C.drop h d c2 c6 λc6:C.drop1 hds c6 c5)
end of h1
(h2)
consider H6
we proved
eq
nat
<λ:PList.nat> CASE PCons h0 d0 hds0 OF PNil⇒d0 | PCons n ⇒n
<λ:PList.nat> CASE PCons h d hds OF PNil⇒d0 | PCons n ⇒n
eq nat d0 d
end of h2
by (h1 h2)
(eq nat h0 h)→(ex2 C λc6:C.drop h d c2 c6 λc6:C.drop1 hds c6 c5)
end of h1
(h2)
consider H5
we proved
eq
nat
<λ:PList.nat> CASE PCons h0 d0 hds0 OF PNil⇒h0 | PCons n ⇒n
<λ:PList.nat> CASE PCons h d hds OF PNil⇒h0 | PCons n ⇒n
eq nat h0 h
end of h2
by (h1 h2)
we proved ex2 C λc6:C.drop h d c2 c6 λc6:C.drop1 hds c6 c5
∀H4:(eq PList (PCons h0 d0 hds0) (PCons h d hds)).(ex2 C λc6:C.drop h d c2 c6 λc6:C.drop1 hds c6 c5)
we proved (eq PList y (PCons h d hds))→(ex2 C λc2:C.drop h d c1 c2 λc2:C.drop1 hds c2 c3)
we proved
∀y:PList
.drop1 y c1 c3
→(eq PList y (PCons h d hds))→(ex2 C λc2:C.drop h d c1 c2 λc2:C.drop1 hds c2 c3)
by (insert_eq . . . . previous H)
we proved ex2 C λc2:C.drop h d c1 c2 λc2:C.drop1 hds c2 c3
we proved
∀c1:C
.∀c3:C
.∀hds:PList
.∀h:nat.∀d:nat.(drop1 (PCons h d hds) c1 c3)→(ex2 C λc2:C.drop h d c1 c2 λc2:C.drop1 hds c2 c3)