DEFINITION aprem_gen_head_S()
TYPE =
∀a1:A.∀a2:A.∀x:A.∀i:nat.(aprem (S i) (AHead a1 a2) x)→(aprem i a2 x)
BODY =
assume a1: A
assume a2: A
assume x: A
assume i: nat
suppose H: aprem (S i) (AHead a1 a2) x
assume y: A
suppose H0: aprem (S i) y x
assume y0: nat
suppose H1: aprem y0 y x
we proceed by induction on H1 to prove (eq nat y0 (S i))→(eq A y (AHead a1 a2))→(aprem i a2 x)
case aprem_zero : a0:A a3:A ⇒
the thesis becomes ∀H2:(eq nat O (S i)).∀H3:(eq A (AHead a0 a3) (AHead a1 a2)).(aprem i a2 a0)
suppose H2: eq nat O (S i)
suppose H3: eq A (AHead a0 a3) (AHead a1 a2)
(H4)
by (f_equal . . . . . H3)
we proved
eq
A
<λ:A.A> CASE AHead a0 a3 OF ASort ⇒a0 | AHead a ⇒a
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a0 | AHead a ⇒a
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a0 | AHead a ⇒a (AHead a0 a3)
λe:A.<λ:A.A> CASE e OF ASort ⇒a0 | AHead a ⇒a (AHead a1 a2)
end of H4
(H6)
consider H4
we proved
eq
A
<λ:A.A> CASE AHead a0 a3 OF ASort ⇒a0 | AHead a ⇒a
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a0 | AHead a ⇒a
eq A a0 a1
end of H6
(H7)
we proceed by induction on H2 to prove <λ:nat.Prop> CASE S i OF O⇒True | S ⇒False
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE O OF O⇒True | S ⇒False
consider I
we proved True
<λ:nat.Prop> CASE O OF O⇒True | S ⇒False
<λ:nat.Prop> CASE S i OF O⇒True | S ⇒False
end of H7
consider H7
we proved <λ:nat.Prop> CASE S i OF O⇒True | S ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove aprem i a2 a1
we proved aprem i a2 a1
by (eq_ind_r . . . previous . H6)
we proved aprem i a2 a0
∀H2:(eq nat O (S i)).∀H3:(eq A (AHead a0 a3) (AHead a1 a2)).(aprem i a2 a0)
case aprem_succ : a0:A a:A i0:nat H2:aprem i0 a0 a a3:A ⇒
the thesis becomes ∀H4:(eq nat (S i0) (S i)).∀H5:(eq A (AHead a3 a0) (AHead a1 a2)).(aprem i a2 a)
(H3) by induction hypothesis we know (eq nat i0 (S i))→(eq A a0 (AHead a1 a2))→(aprem i a2 a)
suppose H4: eq nat (S i0) (S i)
suppose H5: eq A (AHead a3 a0) (AHead a1 a2)
(H6)
by (f_equal . . . . . H5)
we proved
eq
A
<λ:A.A> CASE AHead a3 a0 OF ASort ⇒a3 | AHead a4 ⇒a4
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a3 | AHead a4 ⇒a4
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a3 | AHead a4 ⇒a4 (AHead a3 a0)
λe:A.<λ:A.A> CASE e OF ASort ⇒a3 | AHead a4 ⇒a4 (AHead a1 a2)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
A
<λ:A.A> CASE AHead a3 a0 OF ASort ⇒a0 | AHead a4⇒a4
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a0 | AHead a4⇒a4
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a0 | AHead a4⇒a4 (AHead a3 a0)
λe:A.<λ:A.A> CASE e OF ASort ⇒a0 | AHead a4⇒a4 (AHead a1 a2)
end of H7
suppose : eq A a3 a1
(H9)
consider H7
we proved
eq
A
<λ:A.A> CASE AHead a3 a0 OF ASort ⇒a0 | AHead a4⇒a4
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a0 | AHead a4⇒a4
that is equivalent to eq A a0 a2
we proceed by induction on the previous result to prove (eq nat i0 (S i))→(eq A a2 (AHead a1 a2))→(aprem i a2 a)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
(eq nat i0 (S i))→(eq A a2 (AHead a1 a2))→(aprem i a2 a)
end of H9
(H10)
consider H7
we proved
eq
A
<λ:A.A> CASE AHead a3 a0 OF ASort ⇒a0 | AHead a4⇒a4
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a0 | AHead a4⇒a4
that is equivalent to eq A a0 a2
we proceed by induction on the previous result to prove aprem i0 a2 a
case refl_equal : ⇒
the thesis becomes the hypothesis H2
aprem i0 a2 a
end of H10
(H11)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:nat.nat> CASE S i0 OF O⇒i0 | S n⇒n
<λ:nat.nat> CASE S i OF O⇒i0 | S n⇒n
eq
nat
λe:nat.<λ:nat.nat> CASE e OF O⇒i0 | S n⇒n (S i0)
λe:nat.<λ:nat.nat> CASE e OF O⇒i0 | S n⇒n (S i)
end of H11
(H13)
consider H11
we proved
eq
nat
<λ:nat.nat> CASE S i0 OF O⇒i0 | S n⇒n
<λ:nat.nat> CASE S i OF O⇒i0 | S n⇒n
that is equivalent to eq nat i0 i
we proceed by induction on the previous result to prove aprem i a2 a
case refl_equal : ⇒
the thesis becomes the hypothesis H10
aprem i a2 a
end of H13
consider H13
we proved aprem i a2 a
(eq A a3 a1)→(aprem i a2 a)
end of h1
(h2)
consider H6
we proved
eq
A
<λ:A.A> CASE AHead a3 a0 OF ASort ⇒a3 | AHead a4 ⇒a4
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a3 | AHead a4 ⇒a4
eq A a3 a1
end of h2
by (h1 h2)
we proved aprem i a2 a
∀H4:(eq nat (S i0) (S i)).∀H5:(eq A (AHead a3 a0) (AHead a1 a2)).(aprem i a2 a)
we proved (eq nat y0 (S i))→(eq A y (AHead a1 a2))→(aprem i a2 x)
we proved
∀y0:nat
.aprem y0 y x
→(eq nat y0 (S i))→(eq A y (AHead a1 a2))→(aprem i a2 x)
by (insert_eq . . . . previous H0)
we proved (eq A y (AHead a1 a2))→(aprem i a2 x)
we proved ∀y:A.(aprem (S i) y x)→(eq A y (AHead a1 a2))→(aprem i a2 x)
by (insert_eq . . . . previous H)
we proved aprem i a2 x
we proved ∀a1:A.∀a2:A.∀x:A.∀i:nat.(aprem (S i) (AHead a1 a2) x)→(aprem i a2 x)