DEFINITION wf3_gen_head2()
TYPE =
∀g:G.∀x:C.∀c:C.∀v:T.∀k:K.(wf3 g x (CHead c k v))→(ex B λb:B.eq K k (Bind b))
BODY =
assume g: G
assume x: C
assume c: C
assume v: T
assume k: K
suppose H: wf3 g x (CHead c k v)
assume y: C
suppose H0: wf3 g x y
we proceed by induction on H0 to prove (eq C y (CHead c k v))→(ex B λb:B.eq K k (Bind b))
case wf3_sort : m:nat ⇒
the thesis becomes ∀H1:(eq C (CSort m) (CHead c k v)).(ex B λb:B.eq K k (Bind b))
suppose H1: eq C (CSort m) (CHead c k v)
(H2)
we proceed by induction on H1 to prove <λ:C.Prop> CASE CHead c k v OF CSort ⇒True | CHead ⇒False
case refl_equal : ⇒
the thesis becomes <λ:C.Prop> CASE CSort m OF CSort ⇒True | CHead ⇒False
consider I
we proved True
<λ:C.Prop> CASE CSort m OF CSort ⇒True | CHead ⇒False
<λ:C.Prop> CASE CHead c k v OF CSort ⇒True | CHead ⇒False
end of H2
consider H2
we proved <λ:C.Prop> CASE CHead c k v OF CSort ⇒True | CHead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove ex B λb:B.eq K k (Bind b)
we proved ex B λb:B.eq K k (Bind b)
∀H1:(eq C (CSort m) (CHead c k v)).(ex B λb:B.eq K k (Bind b))
case wf3_bind : c1:C c2:C H1:wf3 g c1 c2 u:T t:T H3:ty3 g c1 u t b:B ⇒
the thesis becomes
∀H4:(eq C (CHead c2 (Bind b) u) (CHead c k v)).(ex B λb0:B.eq K k (Bind b0))
(H2) by induction hypothesis we know (eq C c2 (CHead c k v))→(ex B λb:B.eq K k (Bind b))
suppose H4: eq C (CHead c2 (Bind b) u) (CHead c k v)
(H5)
by (f_equal . . . . . H4)
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c k v OF CSort ⇒c2 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead c2 (Bind b) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead c k v)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
K
<λ:C.K> CASE CHead c2 (Bind b) u OF CSort ⇒Bind b | CHead k0 ⇒k0
<λ:C.K> CASE CHead c k v OF CSort ⇒Bind b | CHead k0 ⇒k0
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒Bind b | CHead k0 ⇒k0
CHead c2 (Bind b) u
λe:C.<λ:C.K> CASE e OF CSort ⇒Bind b | CHead k0 ⇒k0 (CHead c k v)
end of H6
(h1)
(H7)
by (f_equal . . . . . H4)
we proved
eq
T
<λ:C.T> CASE CHead c2 (Bind b) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead c k v OF CSort ⇒u | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead c2 (Bind b) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead c k v)
end of H7
suppose H8: eq K (Bind b) k
suppose H9: eq C c2 c
(H11)
we proceed by induction on H9 to prove (eq C c (CHead c k v))→(ex B λb0:B.eq K k (Bind b0))
case refl_equal : ⇒
the thesis becomes the hypothesis H2
(eq C c (CHead c k v))→(ex B λb0:B.eq K k (Bind b0))
end of H11
we proceed by induction on H8 to prove ex B λb0:B.eq K k (Bind b0)
case refl_equal : ⇒
the thesis becomes ex B λb0:B.eq K (Bind b) (Bind b0)
by (refl_equal . .)
we proved eq K (Bind b) (Bind b)
by (ex_intro . . . previous)
ex B λb0:B.eq K (Bind b) (Bind b0)
we proved ex B λb0:B.eq K k (Bind b0)
(eq K (Bind b) k)→(eq C c2 c)→(ex B λb0:B.eq K k (Bind b0))
end of h1
(h2)
consider H6
we proved
eq
K
<λ:C.K> CASE CHead c2 (Bind b) u OF CSort ⇒Bind b | CHead k0 ⇒k0
<λ:C.K> CASE CHead c k v OF CSort ⇒Bind b | CHead k0 ⇒k0
eq K (Bind b) k
end of h2
by (h1 h2)
(eq C c2 c)→(ex B λb0:B.eq K k (Bind b0))
end of h1
(h2)
consider H5
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c k v OF CSort ⇒c2 | CHead c0 ⇒c0
eq C c2 c
end of h2
by (h1 h2)
we proved ex B λb0:B.eq K k (Bind b0)
∀H4:(eq C (CHead c2 (Bind b) u) (CHead c k v)).(ex B λb0:B.eq K k (Bind b0))
case wf3_void : c1:C c2:C H1:wf3 g c1 c2 u:T :∀t:T.(ty3 g c1 u t)→False :B ⇒
the thesis becomes
∀H4:eq C (CHead c2 (Bind Void) (TSort O)) (CHead c k v)
.ex B λb0:B.eq K k (Bind b0)
(H2) by induction hypothesis we know (eq C c2 (CHead c k v))→(ex B λb:B.eq K k (Bind b))
suppose H4: eq C (CHead c2 (Bind Void) (TSort O)) (CHead c k v)
(H5)
by (f_equal . . . . . H4)
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind Void) (TSort O) OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c k v OF CSort ⇒c2 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0
CHead c2 (Bind Void) (TSort O)
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead c k v)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
K
<λ:C.K>
CASE CHead c2 (Bind Void) (TSort O) OF
CSort ⇒Bind Void
| CHead k0 ⇒k0
<λ:C.K> CASE CHead c k v OF CSort ⇒Bind Void | CHead k0 ⇒k0
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒Bind Void | CHead k0 ⇒k0
CHead c2 (Bind Void) (TSort O)
λe:C.<λ:C.K> CASE e OF CSort ⇒Bind Void | CHead k0 ⇒k0 (CHead c k v)
end of H6
(h1)
(H7)
by (f_equal . . . . . H4)
we proved
eq
T
<λ:C.T>
CASE CHead c2 (Bind Void) (TSort O) OF
CSort ⇒TSort O
| CHead t⇒t
<λ:C.T> CASE CHead c k v OF CSort ⇒TSort O | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒TSort O | CHead t⇒t
CHead c2 (Bind Void) (TSort O)
λe:C.<λ:C.T> CASE e OF CSort ⇒TSort O | CHead t⇒t (CHead c k v)
end of H7
suppose H8: eq K (Bind Void) k
suppose H9: eq C c2 c
(H10)
we proceed by induction on H9 to prove (eq C c (CHead c k v))→(ex B λb0:B.eq K k (Bind b0))
case refl_equal : ⇒
the thesis becomes the hypothesis H2
(eq C c (CHead c k v))→(ex B λb0:B.eq K k (Bind b0))
end of H10
(H12)
by (eq_ind_r . . . H10 . H8)
eq C c (CHead c (Bind Void) v)
→ex B λb0:B.eq K (Bind Void) (Bind b0)
end of H12
we proceed by induction on H8 to prove ex B λb0:B.eq K k (Bind b0)
case refl_equal : ⇒
the thesis becomes ex B λb0:B.eq K (Bind Void) (Bind b0)
by (refl_equal . .)
we proved eq K (Bind Void) (Bind Void)
by (ex_intro . . . previous)
ex B λb0:B.eq K (Bind Void) (Bind b0)
we proved ex B λb0:B.eq K k (Bind b0)
eq K (Bind Void) k
→(eq C c2 c)→(ex B λb0:B.eq K k (Bind b0))
end of h1
(h2)
consider H6
we proved
eq
K
<λ:C.K>
CASE CHead c2 (Bind Void) (TSort O) OF
CSort ⇒Bind Void
| CHead k0 ⇒k0
<λ:C.K> CASE CHead c k v OF CSort ⇒Bind Void | CHead k0 ⇒k0
eq K (Bind Void) k
end of h2
by (h1 h2)
(eq C c2 c)→(ex B λb0:B.eq K k (Bind b0))
end of h1
(h2)
consider H5
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind Void) (TSort O) OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c k v OF CSort ⇒c2 | CHead c0 ⇒c0
eq C c2 c
end of h2
by (h1 h2)
we proved ex B λb0:B.eq K k (Bind b0)
∀H4:eq C (CHead c2 (Bind Void) (TSort O)) (CHead c k v)
.ex B λb0:B.eq K k (Bind b0)
case wf3_flat : c1:C c2:C H1:wf3 g c1 c2 :T :F ⇒
the thesis becomes ∀H3:(eq C c2 (CHead c k v)).(ex B λb:B.eq K k (Bind b))
(H2) by induction hypothesis we know (eq C c2 (CHead c k v))→(ex B λb:B.eq K k (Bind b))
suppose H3: eq C c2 (CHead c k v)
(H4)
by (f_equal . . . . . H3)
we proved eq C c2 (CHead c k v)
eq C (λe:C.e c2) (λe:C.e (CHead c k v))
end of H4
(H5)
we proceed by induction on H4 to prove
eq C (CHead c k v) (CHead c k v)
→ex B λb:B.eq K k (Bind b)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
eq C (CHead c k v) (CHead c k v)
→ex B λb:B.eq K k (Bind b)
end of H5
by (refl_equal . .)
we proved eq C (CHead c k v) (CHead c k v)
by (H5 previous)
we proved ex B λb:B.eq K k (Bind b)
∀H3:(eq C c2 (CHead c k v)).(ex B λb:B.eq K k (Bind b))
we proved (eq C y (CHead c k v))→(ex B λb:B.eq K k (Bind b))
we proved
∀y:C
.wf3 g x y
→(eq C y (CHead c k v))→(ex B λb:B.eq K k (Bind b))
by (insert_eq . . . . previous H)
we proved ex B λb:B.eq K k (Bind b)
we proved ∀g:G.∀x:C.∀c:C.∀v:T.∀k:K.(wf3 g x (CHead c k v))→(ex B λb:B.eq K k (Bind b))