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