DEFINITION drop_mono()
TYPE =
∀c:C.∀x1:C.∀d:nat.∀h:nat.(drop h d c x1)→∀x2:C.(drop h d c x2)→(eq C x1 x2)
BODY =
assume c: C
we proceed by induction on c to prove ∀x1:C.∀d:nat.∀h:nat.(drop h d c x1)→∀x2:C.(drop h d c x2)→(eq C x1 x2)
case CSort : n:nat ⇒
the thesis becomes ∀x1:C.∀d:nat.∀h:nat.∀H:(drop h d (CSort n) x1).∀x2:C.∀H0:(drop h d (CSort n) x2).(eq C x1 x2)
assume x1: C
assume d: nat
assume h: nat
suppose H: drop h d (CSort n) x1
assume x2: C
suppose H0: drop h d (CSort n) x2
by (drop_gen_sort . . . . H0)
we proved and3 (eq C x2 (CSort n)) (eq nat h O) (eq nat d O)
we proceed by induction on the previous result to prove eq C x1 x2
case and3_intro : H1:eq C x2 (CSort n) H2:eq nat h O H3:eq nat d O ⇒
the thesis becomes eq C x1 x2
by (drop_gen_sort . . . . H)
we proved and3 (eq C x1 (CSort n)) (eq nat h O) (eq nat d O)
we proceed by induction on the previous result to prove eq C x1 x2
case and3_intro : H4:eq C x1 (CSort n) H5:eq nat h O H6:eq nat d O ⇒
the thesis becomes eq C x1 x2
by (refl_equal . .)
we proved eq C (CSort n) (CSort n)
by (eq_ind_r . . . previous . H4)
we proved eq C x1 (CSort n)
by (eq_ind_r . . . previous . H1)
eq C x1 x2
eq C x1 x2
we proved eq C x1 x2
∀x1:C.∀d:nat.∀h:nat.∀H:(drop h d (CSort n) x1).∀x2:C.∀H0:(drop h d (CSort n) x2).(eq C x1 x2)
case CHead : c0:C k:K t:T ⇒
the thesis becomes
∀x1:C
.∀d:nat
.∀h:nat
.(drop h d (CHead c0 k t) x1)→∀x2:C.(drop h d (CHead c0 k t) x2)→(eq C x1 x2)
(H) by induction hypothesis we know ∀x1:C.∀d:nat.∀h:nat.(drop h d c0 x1)→∀x2:C.(drop h d c0 x2)→(eq C x1 x2)
assume x1: C
assume d: nat
we proceed by induction on d to prove
∀h:nat
.(drop h d (CHead c0 k t) x1)→∀x2:C.(drop h d (CHead c0 k t) x2)→(eq C x1 x2)
case O : ⇒
the thesis becomes
∀h:nat
.(drop h O (CHead c0 k t) x1)→∀x2:C.(drop h O (CHead c0 k t) x2)→(eq C x1 x2)
assume h: nat
we proceed by induction on h to prove
(drop h O (CHead c0 k t) x1)→∀x2:C.(drop h O (CHead c0 k t) x2)→(eq C x1 x2)
case O : ⇒
the thesis becomes
(drop O O (CHead c0 k t) x1)→∀x2:C.(drop O O (CHead c0 k t) x2)→(eq C x1 x2)
suppose H0: drop O O (CHead c0 k t) x1
assume x2: C
suppose H1: drop O O (CHead c0 k t) x2
by (drop_gen_refl . . H1)
we proved eq C (CHead c0 k t) x2
we proceed by induction on the previous result to prove eq C x1 x2
case refl_equal : ⇒
the thesis becomes eq C x1 (CHead c0 k t)
by (drop_gen_refl . . H0)
we proved eq C (CHead c0 k t) x1
we proceed by induction on the previous result to prove eq C x1 (CHead c0 k t)
case refl_equal : ⇒
the thesis becomes eq C (CHead c0 k t) (CHead c0 k t)
by (refl_equal . .)
eq C (CHead c0 k t) (CHead c0 k t)
eq C x1 (CHead c0 k t)
we proved eq C x1 x2
(drop O O (CHead c0 k t) x1)→∀x2:C.(drop O O (CHead c0 k t) x2)→(eq C x1 x2)
case S : n:nat ⇒
the thesis becomes ∀H1:(drop (S n) O (CHead c0 k t) x1).∀x2:C.∀H2:(drop (S n) O (CHead c0 k t) x2).(eq C x1 x2)
() by induction hypothesis we know
(drop n O (CHead c0 k t) x1)→∀x2:C.(drop n O (CHead c0 k t) x2)→(eq C x1 x2)
suppose H1: drop (S n) O (CHead c0 k t) x1
assume x2: C
suppose H2: drop (S n) O (CHead c0 k t) x2
(h1)
by (drop_gen_drop . . . . . H1)
drop (r k n) O c0 x1
end of h1
(h2)
by (drop_gen_drop . . . . . H2)
drop (r k n) O c0 x2
end of h2
by (H . . . h1 . h2)
we proved eq C x1 x2
∀H1:(drop (S n) O (CHead c0 k t) x1).∀x2:C.∀H2:(drop (S n) O (CHead c0 k t) x2).(eq C x1 x2)
we proved
(drop h O (CHead c0 k t) x1)→∀x2:C.(drop h O (CHead c0 k t) x2)→(eq C x1 x2)
∀h:nat
.(drop h O (CHead c0 k t) x1)→∀x2:C.(drop h O (CHead c0 k t) x2)→(eq C x1 x2)
case S : n:nat ⇒
the thesis becomes
∀h:nat
.∀H1:(drop h (S n) (CHead c0 k t) x1).∀x2:C.∀H2:(drop h (S n) (CHead c0 k t) x2).(eq C x1 x2)
(H0) by induction hypothesis we know
∀h:nat
.(drop h n (CHead c0 k t) x1)→∀x2:C.(drop h n (CHead c0 k t) x2)→(eq C x1 x2)
assume h: nat
suppose H1: drop h (S n) (CHead c0 k t) x1
assume x2: C
suppose H2: drop h (S n) (CHead c0 k t) x2
by (drop_gen_skip_l . . . . . . H2)
we proved
ex3_2
C
T
λe:C.λv:T.eq C x2 (CHead e k v)
λ:C.λv:T.eq T t (lift h (r k n) v)
λe:C.λ:T.drop h (r k n) c0 e
we proceed by induction on the previous result to prove eq C x1 x2
case ex3_2_intro : x0:C x3:T H3:eq C x2 (CHead x0 k x3) H4:eq T t (lift h (r k n) x3) H5:drop h (r k n) c0 x0 ⇒
the thesis becomes eq C x1 x2
by (drop_gen_skip_l . . . . . . H1)
we proved
ex3_2
C
T
λe:C.λv:T.eq C x1 (CHead e k v)
λ:C.λv:T.eq T t (lift h (r k n) v)
λe:C.λ:T.drop h (r k n) c0 e
we proceed by induction on the previous result to prove eq C x1 x2
case ex3_2_intro : x4:C x5:T H6:eq C x1 (CHead x4 k x5) H7:eq T t (lift h (r k n) x5) H8:drop h (r k n) c0 x4 ⇒
the thesis becomes eq C x1 x2
(H9)
we proceed by induction on H6 to prove
∀h0:nat
.drop h0 n (CHead c0 k t) (CHead x4 k x5)
→∀x6:C.(drop h0 n (CHead c0 k t) x6)→(eq C (CHead x4 k x5) x6)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
∀h0:nat
.drop h0 n (CHead c0 k t) (CHead x4 k x5)
→∀x6:C.(drop h0 n (CHead c0 k t) x6)→(eq C (CHead x4 k x5) x6)
end of H9
(H10)
we proceed by induction on H7 to prove
∀h0:nat
.drop h0 n (CHead c0 k (lift h (r k n) x5)) (CHead x4 k x5)
→∀x6:C.(drop h0 n (CHead c0 k (lift h (r k n) x5)) x6)→(eq C (CHead x4 k x5) x6)
case refl_equal : ⇒
the thesis becomes the hypothesis H9
∀h0:nat
.drop h0 n (CHead c0 k (lift h (r k n) x5)) (CHead x4 k x5)
→∀x6:C.(drop h0 n (CHead c0 k (lift h (r k n) x5)) x6)→(eq C (CHead x4 k x5) x6)
end of H10
(H11)
we proceed by induction on H7 to prove eq T (lift h (r k n) x5) (lift h (r k n) x3)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq T (lift h (r k n) x5) (lift h (r k n) x3)
end of H11
(h1)
(h1)
by (H . . . H5 . H8)
we proved eq C x0 x4
by (sym_eq . . . previous)
eq C x4 x0
end of h1
(h2)
by (refl_equal . .)
eq K k k
end of h2
(h3)
by (refl_equal . .)
eq T x3 x3
end of h3
by (f_equal3 . . . . . . . . . . . h1 h2 h3)
eq C (CHead x4 k x3) (CHead x0 k x3)
end of h1
(h2)
by (lift_inj . . . . H11)
eq T x5 x3
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq C (CHead x4 k x5) (CHead x0 k x3)
by (eq_ind_r . . . previous . H6)
we proved eq C x1 (CHead x0 k x3)
by (eq_ind_r . . . previous . H3)
eq C x1 x2
eq C x1 x2
we proved eq C x1 x2
∀h:nat
.∀H1:(drop h (S n) (CHead c0 k t) x1).∀x2:C.∀H2:(drop h (S n) (CHead c0 k t) x2).(eq C x1 x2)
we proved
∀h:nat
.(drop h d (CHead c0 k t) x1)→∀x2:C.(drop h d (CHead c0 k t) x2)→(eq C x1 x2)
∀x1:C
.∀d:nat
.∀h:nat
.(drop h d (CHead c0 k t) x1)→∀x2:C.(drop h d (CHead c0 k t) x2)→(eq C x1 x2)
we proved ∀x1:C.∀d:nat.∀h:nat.(drop h d c x1)→∀x2:C.(drop h d c x2)→(eq C x1 x2)
we proved ∀c:C.∀x1:C.∀d:nat.∀h:nat.(drop h d c x1)→∀x2:C.(drop h d c x2)→(eq C x1 x2)