DEFINITION aprem_repl()
TYPE =
∀g:G
.∀a1:A.∀a2:A.(leq g a1 a2)→∀i:nat.∀b2:A.(aprem i a2 b2)→(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i a1 b1)
BODY =
assume g: G
assume a1: A
assume a2: A
suppose H: leq g a1 a2
we proceed by induction on H to prove ∀i:nat.∀b2:A.(aprem i a2 b2)→(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i a1 b1)
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 ∀i:nat.∀b2:A.∀H1:(aprem i (ASort h2 n2) b2).(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i (ASort h1 n1) b1)
assume i: nat
assume b2: A
suppose H1: aprem i (ASort h2 n2) b2
(H_x)
by (aprem_gen_sort . . . . H1)
False
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i (ASort h1 n1) b1
we proved ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i (ASort h1 n1) b1
∀i:nat.∀b2:A.∀H1:(aprem i (ASort h2 n2) b2).(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i (ASort h1 n1) b1)
case leq_head : a0:A a3:A H0:leq g a0 a3 a4:A a5:A :leq g a4 a5 ⇒
the thesis becomes ∀i:nat.∀b2:A.∀H4:(aprem i (AHead a3 a5) b2).(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i (AHead a0 a4) b1)
() by induction hypothesis we know ∀i:nat.∀b2:A.(aprem i a3 b2)→(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i a0 b1)
(H3) by induction hypothesis we know ∀i:nat.∀b2:A.(aprem i a5 b2)→(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i a4 b1)
assume i: nat
assume b2: A
suppose H4: aprem i (AHead a3 a5) b2
suppose H5: aprem O (AHead a3 a5) b2
(H_y)
by (aprem_gen_head_O . . . H5)
eq A b2 a3
end of H_y
by (aprem_zero . .)
we proved aprem O (AHead a0 a4) a0
by (ex_intro2 . . . . H0 previous)
we proved ex2 A λb1:A.leq g b1 a3 λb1:A.aprem O (AHead a0 a4) b1
by (eq_ind_r . . . previous . H_y)
we proved ex2 A λb1:A.leq g b1 b2 λb1:A.aprem O (AHead a0 a4) b1
(aprem O (AHead a3 a5) b2)→(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem O (AHead a0 a4) b1)
assume i0: nat
suppose : (aprem i0 (AHead a3 a5) b2)→(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i0 (AHead a0 a4) b1)
suppose H5: aprem (S i0) (AHead a3 a5) b2
(H_y)
by (aprem_gen_head_S . . . . H5)
aprem i0 a5 b2
end of H_y
(H_x)
by (H3 . . H_y)
ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i0 a4 b1
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove ex2 A λb1:A.leq g b1 b2 λb1:A.aprem (S i0) (AHead a0 a4) b1
case ex_intro2 : x:A H7:leq g x b2 H8:aprem i0 a4 x ⇒
the thesis becomes ex2 A λb1:A.leq g b1 b2 λb1:A.aprem (S i0) (AHead a0 a4) b1
by (aprem_succ . . . H8 .)
we proved aprem (S i0) (AHead a0 a4) x
by (ex_intro2 . . . . H7 previous)
ex2 A λb1:A.leq g b1 b2 λb1:A.aprem (S i0) (AHead a0 a4) b1
we proved ex2 A λb1:A.leq g b1 b2 λb1:A.aprem (S i0) (AHead a0 a4) b1
∀H5:(aprem (S i0) (AHead a3 a5) b2).(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem (S i0) (AHead a0 a4) b1)
by (previous . H4)
we proved ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i (AHead a0 a4) b1
∀i:nat.∀b2:A.∀H4:(aprem i (AHead a3 a5) b2).(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i (AHead a0 a4) b1)
we proved ∀i:nat.∀b2:A.(aprem i a2 b2)→(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i a1 b1)
we proved
∀g:G
.∀a1:A.∀a2:A.(leq g a1 a2)→∀i:nat.∀b2:A.(aprem i a2 b2)→(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i a1 b1)