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