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