DEFINITION asucc_gen_head()
TYPE =
∀g:G
.∀a1:A
.∀a2:A
.∀a:A
.eq A (AHead a1 a2) (asucc g a)
→ex2 A λa0:A.eq A a (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
BODY =
assume g: G
assume a1: A
assume a2: A
assume a: A
we proceed by induction on a to prove
eq A (AHead a1 a2) (asucc g a)
→ex2 A λa3:A.eq A a (AHead a1 a3) λa3:A.eq A a2 (asucc g a3)
case ASort : n:nat n0:nat ⇒
the thesis becomes
∀H:eq A (AHead a1 a2) (asucc g (ASort n n0))
.ex2 A λa0:A.eq A (ASort n n0) (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
suppose H: eq A (AHead a1 a2) (asucc g (ASort n n0))
suppose H0: eq A (AHead a1 a2) (asucc g (ASort O n0))
(H1)
consider H0
we proved eq A (AHead a1 a2) (asucc g (ASort O n0))
that is equivalent to eq A (AHead a1 a2) (ASort O (next g n0))
we proceed by induction on the previous result to prove <λ:A.Prop> CASE ASort O (next g n0) OF ASort ⇒False | AHead ⇒True
case refl_equal : ⇒
the thesis becomes <λ:A.Prop> CASE AHead a1 a2 OF ASort ⇒False | AHead ⇒True
consider I
we proved True
<λ:A.Prop> CASE AHead a1 a2 OF ASort ⇒False | AHead ⇒True
<λ:A.Prop> CASE ASort O (next g n0) OF ASort ⇒False | AHead ⇒True
end of H1
consider H1
we proved <λ:A.Prop> CASE ASort O (next g n0) OF ASort ⇒False | AHead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove ex2 A λa0:A.eq A (ASort O n0) (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
we proved ex2 A λa0:A.eq A (ASort O n0) (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
eq A (AHead a1 a2) (asucc g (ASort O n0))
→ex2 A λa0:A.eq A (ASort O n0) (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
assume n1: nat
suppose :
eq A (AHead a1 a2) (asucc g (ASort n1 n0))
→ex2 A λa0:A.eq A (ASort n1 n0) (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
suppose H0: eq A (AHead a1 a2) (asucc g (ASort (S n1) n0))
(H1)
consider H0
we proved eq A (AHead a1 a2) (asucc g (ASort (S n1) n0))
that is equivalent to eq A (AHead a1 a2) (ASort n1 n0)
we proceed by induction on the previous result to prove <λ:A.Prop> CASE ASort n1 n0 OF ASort ⇒False | AHead ⇒True
case refl_equal : ⇒
the thesis becomes <λ:A.Prop> CASE AHead a1 a2 OF ASort ⇒False | AHead ⇒True
consider I
we proved True
<λ:A.Prop> CASE AHead a1 a2 OF ASort ⇒False | AHead ⇒True
<λ:A.Prop> CASE ASort n1 n0 OF ASort ⇒False | AHead ⇒True
end of H1
consider H1
we proved <λ:A.Prop> CASE ASort n1 n0 OF ASort ⇒False | AHead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove ex2 A λa0:A.eq A (ASort (S n1) n0) (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
we proved ex2 A λa0:A.eq A (ASort (S n1) n0) (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
∀H0:eq A (AHead a1 a2) (asucc g (ASort (S n1) n0))
.ex2 A λa0:A.eq A (ASort (S n1) n0) (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
by (previous . H)
we proved ex2 A λa0:A.eq A (ASort n n0) (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
∀H:eq A (AHead a1 a2) (asucc g (ASort n n0))
.ex2 A λa0:A.eq A (ASort n n0) (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
case AHead : a0:A a3:A ⇒
the thesis becomes
∀H1:eq A (AHead a1 a2) (asucc g (AHead a0 a3))
.ex2 A λa5:A.eq A (AHead a0 a3) (AHead a1 a5) λa5:A.eq A a2 (asucc g a5)
(H) by induction hypothesis we know
eq A (AHead a1 a2) (asucc g a0)
→ex2 A λa3:A.eq A a0 (AHead a1 a3) λa3:A.eq A a2 (asucc g a3)
(H0) by induction hypothesis we know
eq A (AHead a1 a2) (asucc g a3)
→ex2 A λa4:A.eq A a3 (AHead a1 a4) λa4:A.eq A a2 (asucc g a4)
suppose H1: eq A (AHead a1 a2) (asucc g (AHead a0 a3))
(H2)
consider H1
we proved eq A (AHead a1 a2) (asucc g (AHead a0 a3))
that is equivalent to eq A (AHead a1 a2) (AHead a0 (asucc g a3))
by (f_equal . . . . . previous)
we proved
eq
A
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a1 | AHead a4 ⇒a4
<λ:A.A> CASE AHead a0 (asucc g a3) OF ASort ⇒a1 | AHead a4 ⇒a4
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a1 | AHead a4 ⇒a4 (AHead a1 a2)
λe:A.<λ:A.A> CASE e OF ASort ⇒a1 | AHead a4 ⇒a4 (AHead a0 (asucc g a3))
end of H2
(h1)
(H3)
consider H1
we proved eq A (AHead a1 a2) (asucc g (AHead a0 a3))
that is equivalent to eq A (AHead a1 a2) (AHead a0 (asucc g a3))
by (f_equal . . . . . previous)
we proved
eq
A
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a2 | AHead a4⇒a4
<λ:A.A> CASE AHead a0 (asucc g a3) OF ASort ⇒a2 | AHead a4⇒a4
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a2 | AHead a4⇒a4 (AHead a1 a2)
λe:A.<λ:A.A> CASE e OF ASort ⇒a2 | AHead a4⇒a4 (AHead a0 (asucc g a3))
end of H3
suppose H4: eq A a1 a0
(H5)
by (eq_ind_r . . . H . H4)
eq A (AHead a1 a2) (asucc g a1)
→ex2 A λa5:A.eq A a1 (AHead a1 a5) λa5:A.eq A a2 (asucc g a5)
end of H5
we proceed by induction on H4 to prove ex2 A λa5:A.eq A (AHead a0 a3) (AHead a1 a5) λa5:A.eq A a2 (asucc g a5)
case refl_equal : ⇒
the thesis becomes ex2 A λa5:A.eq A (AHead a1 a3) (AHead a1 a5) λa5:A.eq A a2 (asucc g a5)
(h1)
(h1)
by (refl_equal . .)
eq A (AHead a1 a3) (AHead a1 a3)
end of h1
(h2)
by (refl_equal . .)
eq A (asucc g a3) (asucc g a3)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 A λa4:A.eq A (AHead a1 a3) (AHead a1 a4) λa4:A.eq A (asucc g a3) (asucc g a4)
end of h1
(h2)
consider H3
we proved
eq
A
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a2 | AHead a4⇒a4
<λ:A.A> CASE AHead a0 (asucc g a3) OF ASort ⇒a2 | AHead a4⇒a4
eq A a2 (asucc g a3)
end of h2
by (eq_ind_r . . . h1 . h2)
ex2 A λa5:A.eq A (AHead a1 a3) (AHead a1 a5) λa5:A.eq A a2 (asucc g a5)
we proved ex2 A λa5:A.eq A (AHead a0 a3) (AHead a1 a5) λa5:A.eq A a2 (asucc g a5)
(eq A a1 a0)→(ex2 A λa5:A.eq A (AHead a0 a3) (AHead a1 a5) λa5:A.eq A a2 (asucc g a5))
end of h1
(h2)
consider H2
we proved
eq
A
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a1 | AHead a4 ⇒a4
<λ:A.A> CASE AHead a0 (asucc g a3) OF ASort ⇒a1 | AHead a4 ⇒a4
eq A a1 a0
end of h2
by (h1 h2)
we proved ex2 A λa5:A.eq A (AHead a0 a3) (AHead a1 a5) λa5:A.eq A a2 (asucc g a5)
∀H1:eq A (AHead a1 a2) (asucc g (AHead a0 a3))
.ex2 A λa5:A.eq A (AHead a0 a3) (AHead a1 a5) λa5:A.eq A a2 (asucc g a5)
we proved
eq A (AHead a1 a2) (asucc g a)
→ex2 A λa3:A.eq A a (AHead a1 a3) λa3:A.eq A a2 (asucc g a3)
we proved
∀g:G
.∀a1:A
.∀a2:A
.∀a:A
.eq A (AHead a1 a2) (asucc g a)
→ex2 A λa3:A.eq A a (AHead a1 a3) λa3:A.eq A a2 (asucc g a3)