DEFINITION wcpr0_gen_head()
TYPE =
∀k:K
.∀c1:C
.∀x:C
.∀u1:T
.wcpr0 (CHead c1 k u1) x
→or (eq C x (CHead c1 k u1)) (ex3_2 C T λc2:C.λu2:T.eq C x (CHead c2 k u2) λc2:C.λ:T.wcpr0 c1 c2 λ:C.λu2:T.pr0 u1 u2)
BODY =
assume k: K
assume c1: C
assume x: C
assume u1: T
suppose H: wcpr0 (CHead c1 k u1) x
assume y: C
suppose H0: wcpr0 y x
we proceed by induction on H0 to prove
eq C y (CHead c1 k u1)
→or (eq C x y) (ex3_2 C T λc2:C.λu2:T.eq C x (CHead c2 k u2) λc2:C.λ:T.wcpr0 c1 c2 λ:C.λu2:T.pr0 u1 u2)
case wcpr0_refl : c:C ⇒
the thesis becomes
∀H1:eq C c (CHead c1 k u1)
.or (eq C c c) (ex3_2 C T λc2:C.λu2:T.eq C c (CHead c2 k u2) λc2:C.λ:T.wcpr0 c1 c2 λ:C.λu2:T.pr0 u1 u2)
suppose H1: eq C c (CHead c1 k u1)
(H2)
by (f_equal . . . . . H1)
we proved eq C c (CHead c1 k u1)
eq C (λe:C.e c) (λe:C.e (CHead c1 k u1))
end of H2
by (refl_equal . .)
we proved eq C (CHead c1 k u1) (CHead c1 k u1)
by (or_introl . . previous)
we proved
or
eq C (CHead c1 k u1) (CHead c1 k u1)
ex3_2 C T λc2:C.λu2:T.eq C (CHead c1 k u1) (CHead c2 k u2) λc2:C.λ:T.wcpr0 c1 c2 λ:C.λu2:T.pr0 u1 u2
by (eq_ind_r . . . previous . H2)
we proved or (eq C c c) (ex3_2 C T λc2:C.λu2:T.eq C c (CHead c2 k u2) λc2:C.λ:T.wcpr0 c1 c2 λ:C.λu2:T.pr0 u1 u2)
∀H1:eq C c (CHead c1 k u1)
.or (eq C c c) (ex3_2 C T λc2:C.λu2:T.eq C c (CHead c2 k u2) λc2:C.λ:T.wcpr0 c1 c2 λ:C.λu2:T.pr0 u1 u2)
case wcpr0_comp : c0:C c2:C H1:wcpr0 c0 c2 u0:T u2:T H3:pr0 u0 u2 k0:K ⇒
the thesis becomes
∀H4:eq C (CHead c0 k0 u0) (CHead c1 k u1)
.or
eq C (CHead c2 k0 u2) (CHead c0 k0 u0)
ex3_2 C T λc3:C.λu3:T.eq C (CHead c2 k0 u2) (CHead c3 k u3) λc3:C.λ:T.wcpr0 c1 c3 λ:C.λu3:T.pr0 u1 u3
(H2) by induction hypothesis we know
eq C c0 (CHead c1 k u1)
→or (eq C c2 c0) (ex3_2 C T λc3:C.λu2:T.eq C c2 (CHead c3 k u2) λc3:C.λ:T.wcpr0 c1 c3 λ:C.λu2:T.pr0 u1 u2)
suppose H4: eq C (CHead c0 k0 u0) (CHead c1 k u1)
(H5)
by (f_equal . . . . . H4)
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 u0 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k u1 OF CSort ⇒c0 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c0 k0 u0)
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c1 k u1)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c1 k u1 OF CSort ⇒k0 | CHead k1 ⇒k1
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c0 k0 u0)
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c1 k u1)
end of H6
(h1)
(H7)
by (f_equal . . . . . H4)
we proved
eq
T
<λ:C.T> CASE CHead c0 k0 u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead c1 k u1 OF CSort ⇒u0 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t⇒t (CHead c0 k0 u0)
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t⇒t (CHead c1 k u1)
end of H7
suppose H8: eq K k0 k
suppose H9: eq C c0 c1
(H10)
consider H7
we proved
eq
T
<λ:C.T> CASE CHead c0 k0 u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead c1 k u1 OF CSort ⇒u0 | CHead t⇒t
that is equivalent to eq T u0 u1
we proceed by induction on the previous result to prove pr0 u1 u2
case refl_equal : ⇒
the thesis becomes the hypothesis H3
pr0 u1 u2
end of H10
(h1)
(H12)
we proceed by induction on H9 to prove wcpr0 c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
wcpr0 c1 c2
end of H12
by (refl_equal . .)
we proved eq C (CHead c2 k u2) (CHead c2 k u2)
by (ex3_2_intro . . . . . . . previous H12 H10)
we proved ex3_2 C T λc3:C.λu3:T.eq C (CHead c2 k u2) (CHead c3 k u3) λc3:C.λ:T.wcpr0 c1 c3 λ:C.λu3:T.pr0 u1 u3
by (or_intror . . previous)
we proved
or
eq C (CHead c2 k u2) (CHead c1 k u1)
ex3_2 C T λc3:C.λu3:T.eq C (CHead c2 k u2) (CHead c3 k u3) λc3:C.λ:T.wcpr0 c1 c3 λ:C.λu3:T.pr0 u1 u3
by (eq_ind_r . . . previous . H9)
or
eq C (CHead c2 k u2) (CHead c0 k u1)
ex3_2 C T λc3:C.λu3:T.eq C (CHead c2 k u2) (CHead c3 k u3) λc3:C.λ:T.wcpr0 c1 c3 λ:C.λu3:T.pr0 u1 u3
end of h1
(h2)
consider H7
we proved
eq
T
<λ:C.T> CASE CHead c0 k0 u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead c1 k u1 OF CSort ⇒u0 | CHead t⇒t
eq T u0 u1
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
eq C (CHead c2 k u2) (CHead c0 k u0)
ex3_2 C T λc3:C.λu3:T.eq C (CHead c2 k u2) (CHead c3 k u3) λc3:C.λ:T.wcpr0 c1 c3 λ:C.λu3:T.pr0 u1 u3
by (eq_ind_r . . . previous . H8)
we proved
or
eq C (CHead c2 k0 u2) (CHead c0 k0 u0)
ex3_2 C T λc3:C.λu3:T.eq C (CHead c2 k0 u2) (CHead c3 k u3) λc3:C.λ:T.wcpr0 c1 c3 λ:C.λu3:T.pr0 u1 u3
eq K k0 k
→(eq C c0 c1
→(or
eq C (CHead c2 k0 u2) (CHead c0 k0 u0)
ex3_2 C T λc3:C.λu3:T.eq C (CHead c2 k0 u2) (CHead c3 k u3) λc3:C.λ:T.wcpr0 c1 c3 λ:C.λu3:T.pr0 u1 u3))
end of h1
(h2)
consider H6
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c1 k u1 OF CSort ⇒k0 | CHead k1 ⇒k1
eq K k0 k
end of h2
by (h1 h2)
eq C c0 c1
→(or
eq C (CHead c2 k0 u2) (CHead c0 k0 u0)
ex3_2 C T λc3:C.λu3:T.eq C (CHead c2 k0 u2) (CHead c3 k u3) λc3:C.λ:T.wcpr0 c1 c3 λ:C.λu3:T.pr0 u1 u3)
end of h1
(h2)
consider H5
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 u0 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k u1 OF CSort ⇒c0 | CHead c ⇒c
eq C c0 c1
end of h2
by (h1 h2)
we proved
or
eq C (CHead c2 k0 u2) (CHead c0 k0 u0)
ex3_2 C T λc3:C.λu3:T.eq C (CHead c2 k0 u2) (CHead c3 k u3) λc3:C.λ:T.wcpr0 c1 c3 λ:C.λu3:T.pr0 u1 u3
∀H4:eq C (CHead c0 k0 u0) (CHead c1 k u1)
.or
eq C (CHead c2 k0 u2) (CHead c0 k0 u0)
ex3_2 C T λc3:C.λu3:T.eq C (CHead c2 k0 u2) (CHead c3 k u3) λc3:C.λ:T.wcpr0 c1 c3 λ:C.λu3:T.pr0 u1 u3
we proved
eq C y (CHead c1 k u1)
→or (eq C x y) (ex3_2 C T λc2:C.λu2:T.eq C x (CHead c2 k u2) λc2:C.λ:T.wcpr0 c1 c2 λ:C.λu2:T.pr0 u1 u2)
we proved
∀y:C
.wcpr0 y x
→(eq C y (CHead c1 k u1)
→or (eq C x y) (ex3_2 C T λc2:C.λu2:T.eq C x (CHead c2 k u2) λc2:C.λ:T.wcpr0 c1 c2 λ:C.λu2:T.pr0 u1 u2))
by (insert_eq . . . . previous H)
we proved or (eq C x (CHead c1 k u1)) (ex3_2 C T λc2:C.λu2:T.eq C x (CHead c2 k u2) λc2:C.λ:T.wcpr0 c1 c2 λ:C.λu2:T.pr0 u1 u2)
we proved
∀k:K
.∀c1:C
.∀x:C
.∀u1:T
.wcpr0 (CHead c1 k u1) x
→or (eq C x (CHead c1 k u1)) (ex3_2 C T λc2:C.λu2:T.eq C x (CHead c2 k u2) λc2:C.λ:T.wcpr0 c1 c2 λ:C.λu2:T.pr0 u1 u2)