DEFINITION leq_gen_head2()
TYPE =
∀g:G
.∀a1:A
.∀a2:A
.∀a:A
.leq g a (AHead a1 a2)
→ex3_2 A A λa3:A.λ:A.leq g a3 a1 λ:A.λa4:A.leq g a4 a2 λa3:A.λa4:A.eq A a (AHead a3 a4)
BODY =
assume g: G
assume a1: A
assume a2: A
assume a: A
suppose H: leq g a (AHead a1 a2)
assume y: A
suppose H0: leq g a y
we proceed by induction on H0 to prove
eq A y (AHead a1 a2)
→ex3_2 A A λa4:A.λ:A.leq g a4 a1 λ:A.λa5:A.leq g a5 a2 λa4:A.λa5:A.eq A a (AHead a4 a5)
case leq_sort : h1:nat h2:nat n1:nat n2:nat k:nat :eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k) ⇒
the thesis becomes
∀H2:eq A (ASort h2 n2) (AHead a1 a2)
.ex3_2 A A λa3:A.λ:A.leq g a3 a1 λ:A.λa4:A.leq g a4 a2 λa3:A.λa4:A.eq A (ASort h1 n1) (AHead a3 a4)
suppose H2: eq A (ASort h2 n2) (AHead a1 a2)
(H3)
we proceed by induction on H2 to prove <λ:A.Prop> CASE AHead a1 a2 OF ASort ⇒True | AHead ⇒False
case refl_equal : ⇒
the thesis becomes <λ:A.Prop> CASE ASort h2 n2 OF ASort ⇒True | AHead ⇒False
consider I
we proved True
<λ:A.Prop> CASE ASort h2 n2 OF ASort ⇒True | AHead ⇒False
<λ:A.Prop> CASE AHead a1 a2 OF ASort ⇒True | AHead ⇒False
end of H3
consider H3
we proved <λ:A.Prop> CASE AHead a1 a2 OF ASort ⇒True | AHead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove ex3_2 A A λa3:A.λ:A.leq g a3 a1 λ:A.λa4:A.leq g a4 a2 λa3:A.λa4:A.eq A (ASort h1 n1) (AHead a3 a4)
we proved ex3_2 A A λa3:A.λ:A.leq g a3 a1 λ:A.λa4:A.leq g a4 a2 λa3:A.λa4:A.eq A (ASort h1 n1) (AHead a3 a4)
∀H2:eq A (ASort h2 n2) (AHead a1 a2)
.ex3_2 A A λa3:A.λ:A.leq g a3 a1 λ:A.λa4:A.leq g a4 a2 λa3:A.λa4:A.eq A (ASort h1 n1) (AHead a3 a4)
case leq_head : a0:A a3:A H1:leq g a0 a3 a4:A a5:A H3:leq g a4 a5 ⇒
the thesis becomes
∀H5:eq A (AHead a3 a5) (AHead a1 a2)
.ex3_2 A A λa6:A.λ:A.leq g a6 a1 λ:A.λa7:A.leq g a7 a2 λa6:A.λa7:A.eq A (AHead a0 a4) (AHead a6 a7)
(H2) by induction hypothesis we know
eq A a3 (AHead a1 a2)
→ex3_2 A A λa4:A.λ:A.leq g a4 a1 λ:A.λa5:A.leq g a5 a2 λa4:A.λa5:A.eq A a0 (AHead a4 a5)
(H4) by induction hypothesis we know
eq A a5 (AHead a1 a2)
→ex3_2 A A λa6:A.λ:A.leq g a6 a1 λ:A.λa7:A.leq g a7 a2 λa6:A.λa7:A.eq A a4 (AHead a6 a7)
suppose H5: eq A (AHead a3 a5) (AHead a1 a2)
(H6)
by (f_equal . . . . . H5)
we proved
eq
A
<λ:A.A> CASE AHead a3 a5 OF ASort ⇒a3 | AHead a6 ⇒a6
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a3 | AHead a6 ⇒a6
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a3 | AHead a6 ⇒a6 (AHead a3 a5)
λe:A.<λ:A.A> CASE e OF ASort ⇒a3 | AHead a6 ⇒a6 (AHead a1 a2)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
A
<λ:A.A> CASE AHead a3 a5 OF ASort ⇒a5 | AHead a6⇒a6
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a5 | AHead a6⇒a6
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a5 | AHead a6⇒a6 (AHead a3 a5)
λe:A.<λ:A.A> CASE e OF ASort ⇒a5 | AHead a6⇒a6 (AHead a1 a2)
end of H7
suppose H8: eq A a3 a1
(H10)
consider H7
we proved
eq
A
<λ:A.A> CASE AHead a3 a5 OF ASort ⇒a5 | AHead a6⇒a6
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a5 | AHead a6⇒a6
that is equivalent to eq A a5 a2
we proceed by induction on the previous result to prove leq g a4 a2
case refl_equal : ⇒
the thesis becomes the hypothesis H3
leq g a4 a2
end of H10
(H12)
we proceed by induction on H8 to prove leq g a0 a1
case refl_equal : ⇒
the thesis becomes the hypothesis H1
leq g a0 a1
end of H12
by (refl_equal . .)
we proved eq A (AHead a0 a4) (AHead a0 a4)
by (ex3_2_intro . . . . . . . H12 H10 previous)
we proved ex3_2 A A λa6:A.λ:A.leq g a6 a1 λ:A.λa7:A.leq g a7 a2 λa6:A.λa7:A.eq A (AHead a0 a4) (AHead a6 a7)
eq A a3 a1
→ex3_2 A A λa6:A.λ:A.leq g a6 a1 λ:A.λa7:A.leq g a7 a2 λa6:A.λa7:A.eq A (AHead a0 a4) (AHead a6 a7)
end of h1
(h2)
consider H6
we proved
eq
A
<λ:A.A> CASE AHead a3 a5 OF ASort ⇒a3 | AHead a6 ⇒a6
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a3 | AHead a6 ⇒a6
eq A a3 a1
end of h2
by (h1 h2)
we proved ex3_2 A A λa6:A.λ:A.leq g a6 a1 λ:A.λa7:A.leq g a7 a2 λa6:A.λa7:A.eq A (AHead a0 a4) (AHead a6 a7)
∀H5:eq A (AHead a3 a5) (AHead a1 a2)
.ex3_2 A A λa6:A.λ:A.leq g a6 a1 λ:A.λa7:A.leq g a7 a2 λa6:A.λa7:A.eq A (AHead a0 a4) (AHead a6 a7)
we proved
eq A y (AHead a1 a2)
→ex3_2 A A λa4:A.λ:A.leq g a4 a1 λ:A.λa5:A.leq g a5 a2 λa4:A.λa5:A.eq A a (AHead a4 a5)
we proved
∀y:A
.leq g a y
→(eq A y (AHead a1 a2)
→ex3_2 A A λa4:A.λ:A.leq g a4 a1 λ:A.λa5:A.leq g a5 a2 λa4:A.λa5:A.eq A a (AHead a4 a5))
by (insert_eq . . . . previous H)
we proved ex3_2 A A λa3:A.λ:A.leq g a3 a1 λ:A.λa4:A.leq g a4 a2 λa3:A.λa4:A.eq A a (AHead a3 a4)
we proved
∀g:G
.∀a1:A
.∀a2:A
.∀a:A
.leq g a (AHead a1 a2)
→ex3_2 A A λa3:A.λ:A.leq g a3 a1 λ:A.λa4:A.leq g a4 a2 λa3:A.λa4:A.eq A a (AHead a3 a4)