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