DEFINITION leq_ahead_false_2()
TYPE =
∀g:G.∀a2:A.∀a1:A.(leq g (AHead a1 a2) a2)→∀P:Prop.P
BODY =
assume g: G
assume a2: A
we proceed by induction on a2 to prove ∀a1:A.(leq g (AHead a1 a2) a2)→∀P:Prop.P
case ASort : n:nat n0:nat ⇒
the thesis becomes ∀a1:A.∀H:(leq g (AHead a1 (ASort n n0)) (ASort n n0)).∀P:Prop.P
assume a1: A
suppose H: leq g (AHead a1 (ASort n n0)) (ASort n n0)
assume P: Prop
suppose H0: leq g (AHead a1 (ASort O n0)) (ASort O n0)
(H_x)
by (leq_gen_head1 . . . . H0)
ex3_2
A
A
λa3:A.λ:A.leq g a1 a3
λ:A.λa4:A.leq g (ASort O n0) 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 a1 x0 :leq g (ASort O n0) 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 a1 (ASort O n0)) (ASort O n0))→P
assume n1: nat
suppose : (leq g (AHead a1 (ASort n1 n0)) (ASort n1 n0))→P
suppose H0: leq g (AHead a1 (ASort (S n1) n0)) (ASort (S n1) n0)
(H_x)
by (leq_gen_head1 . . . . H0)
ex3_2
A
A
λa3:A.λ:A.leq g a1 a3
λ:A.λa4:A.leq g (ASort (S n1) n0) 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 a1 x0 :leq g (ASort (S n1) n0) 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 a1 (ASort (S n1) n0)) (ASort (S n1) n0)).P
by (previous . H)
we proved P
∀a1:A.∀H:(leq g (AHead a1 (ASort n n0)) (ASort n n0)).∀P:Prop.P
case AHead : a:A a0:A ⇒
the thesis becomes ∀a1:A.∀H1:(leq g (AHead a1 (AHead a a0)) (AHead a a0)).∀P:Prop.P
() by induction hypothesis we know ∀a1:A.(leq g (AHead a1 a) a)→∀P:Prop.P
(H0) by induction hypothesis we know ∀a1:A.(leq g (AHead a1 a0) a0)→∀P:Prop.P
assume a1: A
suppose H1: leq g (AHead a1 (AHead a a0)) (AHead a a0)
assume P: Prop
(H_x)
by (leq_gen_head1 . . . . H1)
ex3_2
A
A
λa3:A.λ:A.leq g a1 a3
λ:A.λa4:A.leq g (AHead a a0) 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 a1 x0 H4:leq g (AHead a a0) 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
(H9)
consider H7
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
that is equivalent to eq A a0 x1
by (eq_ind_r . . . H4 . previous)
leq g (AHead a a0) a0
end of H9
by (H0 . H9 .)
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
∀a1:A.∀H1:(leq g (AHead a1 (AHead a a0)) (AHead a a0)).∀P:Prop.P
we proved ∀a1:A.(leq g (AHead a1 a2) a2)→∀P:Prop.P
we proved ∀g:G.∀a2:A.∀a1:A.(leq g (AHead a1 a2) a2)→∀P:Prop.P