DEFINITION wf3_mono()
TYPE =
∀g:G.∀c:C.∀c1:C.(wf3 g c c1)→∀c2:C.(wf3 g c c2)→(eq C c1 c2)
BODY =
assume g: G
assume c: C
assume c1: C
suppose H: wf3 g c c1
we proceed by induction on H to prove ∀c3:C.(wf3 g c c3)→(eq C c1 c3)
case wf3_sort : m:nat ⇒
the thesis becomes ∀c2:C.∀H0:(wf3 g (CSort m) c2).(eq C (CSort m) c2)
assume c2: C
suppose H0: wf3 g (CSort m) c2
(H_y)
by (wf3_gen_sort1 . . . H0)
eq C c2 (CSort m)
end of H_y
by (refl_equal . .)
we proved eq C (CSort m) (CSort m)
by (eq_ind_r . . . previous . H_y)
we proved eq C (CSort m) c2
∀c2:C.∀H0:(wf3 g (CSort m) c2).(eq C (CSort m) c2)
case wf3_bind : c2:C c3:C :wf3 g c2 c3 u:T t:T H2:ty3 g c2 u t b:B ⇒
the thesis becomes ∀c0:C.∀H3:(wf3 g (CHead c2 (Bind b) u) c0).(eq C (CHead c3 (Bind b) u) c0)
(H1) by induction hypothesis we know ∀c4:C.(wf3 g c2 c4)→(eq C c3 c4)
assume c0: C
suppose H3: wf3 g (CHead c2 (Bind b) u) c0
(H_x)
by (wf3_gen_bind1 . . . . . H3)
or
ex3_2 C T λc2:C.λ:T.eq C c0 (CHead c2 (Bind b) u) λc2:C.λ:T.wf3 g c2 c2 λ:C.λw:T.ty3 g c2 u w
ex3
C
λc2:C.eq C c0 (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c2 c2
λ:C.∀w:T.(ty3 g c2 u w)→False
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove eq C (CHead c3 (Bind b) u) c0
case or_introl : H5:ex3_2 C T λc4:C.λ:T.eq C c0 (CHead c4 (Bind b) u) λc4:C.λ:T.wf3 g c2 c4 λ:C.λw:T.ty3 g c2 u w ⇒
the thesis becomes eq C (CHead c3 (Bind b) u) c0
we proceed by induction on H5 to prove eq C (CHead c3 (Bind b) u) c0
case ex3_2_intro : x0:C x1:T H6:eq C c0 (CHead x0 (Bind b) u) H7:wf3 g c2 x0 :ty3 g c2 u x1 ⇒
the thesis becomes eq C (CHead c3 (Bind b) u) c0
(h1) by (H1 . H7) we proved eq C c3 x0
(h2)
by (refl_equal . .)
eq K (Bind b) (Bind b)
end of h2
(h3)
by (refl_equal . .)
eq T u u
end of h3
by (f_equal3 . . . . . . . . . . . h1 h2 h3)
we proved eq C (CHead c3 (Bind b) u) (CHead x0 (Bind b) u)
by (eq_ind_r . . . previous . H6)
eq C (CHead c3 (Bind b) u) c0
eq C (CHead c3 (Bind b) u) c0
case or_intror : H5:ex3 C λc4:C.eq C c0 (CHead c4 (Bind Void) (TSort O)) λc4:C.wf3 g c2 c4 λ:C.∀w:T.(ty3 g c2 u w)→False ⇒
the thesis becomes eq C (CHead c3 (Bind b) u) c0
we proceed by induction on H5 to prove eq C (CHead c3 (Bind b) u) c0
case ex3_intro : x0:C H6:eq C c0 (CHead x0 (Bind Void) (TSort O)) :wf3 g c2 x0 H8:∀w:T.(ty3 g c2 u w)→False ⇒
the thesis becomes eq C (CHead c3 (Bind b) u) c0
(H_x0) by (H8 . H2) we proved False
(H9) consider H_x0
we proceed by induction on H9 to prove eq C (CHead c3 (Bind b) u) (CHead x0 (Bind Void) (TSort O))
we proved eq C (CHead c3 (Bind b) u) (CHead x0 (Bind Void) (TSort O))
by (eq_ind_r . . . previous . H6)
eq C (CHead c3 (Bind b) u) c0
eq C (CHead c3 (Bind b) u) c0
we proved eq C (CHead c3 (Bind b) u) c0
∀c0:C.∀H3:(wf3 g (CHead c2 (Bind b) u) c0).(eq C (CHead c3 (Bind b) u) c0)
case wf3_void : c2:C c3:C :wf3 g c2 c3 u:T H2:∀t:T.(ty3 g c2 u t)→False b:B ⇒
the thesis becomes
∀c0:C
.∀H3:(wf3 g (CHead c2 (Bind b) u) c0).(eq C (CHead c3 (Bind Void) (TSort O)) c0)
(H1) by induction hypothesis we know ∀c4:C.(wf3 g c2 c4)→(eq C c3 c4)
assume c0: C
suppose H3: wf3 g (CHead c2 (Bind b) u) c0
(H_x)
by (wf3_gen_bind1 . . . . . H3)
or
ex3_2 C T λc2:C.λ:T.eq C c0 (CHead c2 (Bind b) u) λc2:C.λ:T.wf3 g c2 c2 λ:C.λw:T.ty3 g c2 u w
ex3
C
λc2:C.eq C c0 (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c2 c2
λ:C.∀w:T.(ty3 g c2 u w)→False
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove eq C (CHead c3 (Bind Void) (TSort O)) c0
case or_introl : H5:ex3_2 C T λc4:C.λ:T.eq C c0 (CHead c4 (Bind b) u) λc4:C.λ:T.wf3 g c2 c4 λ:C.λw:T.ty3 g c2 u w ⇒
the thesis becomes eq C (CHead c3 (Bind Void) (TSort O)) c0
we proceed by induction on H5 to prove eq C (CHead c3 (Bind Void) (TSort O)) c0
case ex3_2_intro : x0:C x1:T H6:eq C c0 (CHead x0 (Bind b) u) :wf3 g c2 x0 H8:ty3 g c2 u x1 ⇒
the thesis becomes eq C (CHead c3 (Bind Void) (TSort O)) c0
(H_x0) by (H2 . H8) we proved False
(H9) consider H_x0
we proceed by induction on H9 to prove eq C (CHead c3 (Bind Void) (TSort O)) (CHead x0 (Bind b) u)
we proved eq C (CHead c3 (Bind Void) (TSort O)) (CHead x0 (Bind b) u)
by (eq_ind_r . . . previous . H6)
eq C (CHead c3 (Bind Void) (TSort O)) c0
eq C (CHead c3 (Bind Void) (TSort O)) c0
case or_intror : H5:ex3 C λc4:C.eq C c0 (CHead c4 (Bind Void) (TSort O)) λc4:C.wf3 g c2 c4 λ:C.∀w:T.(ty3 g c2 u w)→False ⇒
the thesis becomes eq C (CHead c3 (Bind Void) (TSort O)) c0
we proceed by induction on H5 to prove eq C (CHead c3 (Bind Void) (TSort O)) c0
case ex3_intro : x0:C H6:eq C c0 (CHead x0 (Bind Void) (TSort O)) H7:wf3 g c2 x0 :∀w:T.(ty3 g c2 u w)→False ⇒
the thesis becomes eq C (CHead c3 (Bind Void) (TSort O)) c0
(h1) by (H1 . H7) we proved eq C c3 x0
(h2)
by (refl_equal . .)
eq K (Bind Void) (Bind Void)
end of h2
(h3)
by (refl_equal . .)
eq T (TSort O) (TSort O)
end of h3
by (f_equal3 . . . . . . . . . . . h1 h2 h3)
we proved
eq
C
CHead c3 (Bind Void) (TSort O)
CHead x0 (Bind Void) (TSort O)
by (eq_ind_r . . . previous . H6)
eq C (CHead c3 (Bind Void) (TSort O)) c0
eq C (CHead c3 (Bind Void) (TSort O)) c0
we proved eq C (CHead c3 (Bind Void) (TSort O)) c0
∀c0:C
.∀H3:(wf3 g (CHead c2 (Bind b) u) c0).(eq C (CHead c3 (Bind Void) (TSort O)) c0)
case wf3_flat : c2:C c3:C :wf3 g c2 c3 u:T f:F ⇒
the thesis becomes ∀c0:C.∀H2:(wf3 g (CHead c2 (Flat f) u) c0).(eq C c3 c0)
(H1) by induction hypothesis we know ∀c4:C.(wf3 g c2 c4)→(eq C c3 c4)
assume c0: C
suppose H2: wf3 g (CHead c2 (Flat f) u) c0
(H_y) by (wf3_gen_flat1 . . . . . H2) we proved wf3 g c2 c0
by (H1 . H_y)
we proved eq C c3 c0
∀c0:C.∀H2:(wf3 g (CHead c2 (Flat f) u) c0).(eq C c3 c0)
we proved ∀c3:C.(wf3 g c c3)→(eq C c1 c3)
we proved ∀g:G.∀c:C.∀c1:C.(wf3 g c c1)→∀c3:C.(wf3 g c c3)→(eq C c1 c3)