DEFINITION sn3_cdelta()
TYPE =
∀v:T
.∀t:T
.∀i:nat
.∀w:T.(ex T λu:T.subst0 i w t u)
→∀c:C.∀d:C.(getl i c (CHead d (Bind Abbr) v))→(sn3 c t)→(sn3 d v)
BODY =
assume v: T
assume t: T
assume i: nat
suppose H: ∀w:T.(ex T λu:T.subst0 i w t u)
(H_x)
by (H .)
ex T λu:T.subst0 i v t u
end of H_x
(H0) consider H_x
we proceed by induction on H0 to prove ∀c:C.∀d:C.(getl i c (CHead d (Bind Abbr) v))→(sn3 c t)→(sn3 d v)
case ex_intro : x:T H1:subst0 i v t x ⇒
the thesis becomes ∀c:C.∀d:C.(getl i c (CHead d (Bind Abbr) v))→(sn3 c t)→(sn3 d v)
we proceed by induction on H1 to prove ∀c:C.∀d:C.(getl i c (CHead d (Bind Abbr) v))→(sn3 c t)→(sn3 d v)
case subst0_lref : v0:T i0:nat ⇒
the thesis becomes ∀c:C.∀d:C.∀H2:(getl i0 c (CHead d (Bind Abbr) v0)).∀H3:(sn3 c (TLRef i0)).(sn3 d v0)
assume c: C
assume d: C
suppose H2: getl i0 c (CHead d (Bind Abbr) v0)
suppose H3: sn3 c (TLRef i0)
by (sn3_gen_def . . . . H2 H3)
we proved sn3 d v0
∀c:C.∀d:C.∀H2:(getl i0 c (CHead d (Bind Abbr) v0)).∀H3:(sn3 c (TLRef i0)).(sn3 d v0)
case subst0_fst : v0:T u2:T u1:T i0:nat :subst0 i0 v0 u1 u2 t0:T k:K ⇒
the thesis becomes ∀c:C.∀d:C.∀H4:(getl i0 c (CHead d (Bind Abbr) v0)).∀H5:(sn3 c (THead k u1 t0)).(sn3 d v0)
(H3) by induction hypothesis we know ∀c:C.∀d:C.(getl i0 c (CHead d (Bind Abbr) v0))→(sn3 c u1)→(sn3 d v0)
assume c: C
assume d: C
suppose H4: getl i0 c (CHead d (Bind Abbr) v0)
suppose H5: sn3 c (THead k u1 t0)
(H_y)
by (sn3_gen_head . . . . H5)
sn3 c u1
end of H_y
by (H3 . . H4 H_y)
we proved sn3 d v0
∀c:C.∀d:C.∀H4:(getl i0 c (CHead d (Bind Abbr) v0)).∀H5:(sn3 c (THead k u1 t0)).(sn3 d v0)
case subst0_snd : k:K v0:T t2:T t1:T i0:nat H2:subst0 (s k i0) v0 t1 t2 u:T ⇒
the thesis becomes ∀c:C.∀d:C.∀H4:(getl i0 c (CHead d (Bind Abbr) v0)).∀H5:(sn3 c (THead k u t1)).(sn3 d v0)
(H3) by induction hypothesis we know
∀c:C.∀d:C.(getl (s k i0) c (CHead d (Bind Abbr) v0))→(sn3 c t1)→(sn3 d v0)
assume c: C
assume d: C
suppose H4: getl i0 c (CHead d (Bind Abbr) v0)
suppose H5: sn3 c (THead k u t1)
assume b: B
suppose : subst0 (s (Bind b) i0) v0 t1 t2
suppose H7:
∀c0:C
.∀d0:C.(getl (s (Bind b) i0) c0 (CHead d0 (Bind Abbr) v0))→(sn3 c0 t1)→(sn3 d0 v0)
suppose H8: sn3 c (THead (Bind b) u t1)
(H_x0)
by (sn3_gen_bind . . . . H8)
land (sn3 c u) (sn3 (CHead c (Bind b) u) t1)
end of H_x0
(H9) consider H_x0
we proceed by induction on H9 to prove sn3 d v0
case conj : :sn3 c u H11:sn3 (CHead c (Bind b) u) t1 ⇒
the thesis becomes sn3 d v0
by (clear_bind . . .)
we proved clear (CHead c (Bind b) u) (CHead c (Bind b) u)
by (getl_clear_bind . . . . previous . . H4)
we proved getl (S i0) (CHead c (Bind b) u) (CHead d (Bind Abbr) v0)
that is equivalent to
getl
s (Bind b) i0
CHead c (Bind b) u
CHead d (Bind Abbr) v0
by (H7 . . previous H11)
sn3 d v0
we proved sn3 d v0
subst0 (s (Bind b) i0) v0 t1 t2
→∀H7:∀c0:C
.∀d0:C.(getl (s (Bind b) i0) c0 (CHead d0 (Bind Abbr) v0))→(sn3 c0 t1)→(sn3 d0 v0)
.∀H8:(sn3 c (THead (Bind b) u t1)).(sn3 d v0)
assume f: F
suppose : subst0 (s (Flat f) i0) v0 t1 t2
suppose H7:
∀c0:C
.∀d0:C.(getl (s (Flat f) i0) c0 (CHead d0 (Bind Abbr) v0))→(sn3 c0 t1)→(sn3 d0 v0)
suppose H8: sn3 c (THead (Flat f) u t1)
(H_x0)
by (sn3_gen_flat . . . . H8)
land (sn3 c u) (sn3 c t1)
end of H_x0
(H9) consider H_x0
we proceed by induction on H9 to prove sn3 d v0
case conj : :sn3 c u H11:sn3 c t1 ⇒
the thesis becomes sn3 d v0
consider H4
we proved getl i0 c (CHead d (Bind Abbr) v0)
that is equivalent to getl (s (Flat f) i0) c (CHead d (Bind Abbr) v0)
by (H7 . . previous H11)
sn3 d v0
we proved sn3 d v0
subst0 (s (Flat f) i0) v0 t1 t2
→∀H7:∀c0:C
.∀d0:C.(getl (s (Flat f) i0) c0 (CHead d0 (Bind Abbr) v0))→(sn3 c0 t1)→(sn3 d0 v0)
.∀H8:(sn3 c (THead (Flat f) u t1)).(sn3 d v0)
by (previous . H2 H3 H5)
we proved sn3 d v0
∀c:C.∀d:C.∀H4:(getl i0 c (CHead d (Bind Abbr) v0)).∀H5:(sn3 c (THead k u t1)).(sn3 d v0)
case subst0_both : v0:T u1:T u2:T i0:nat :subst0 i0 v0 u1 u2 k:K t1:T t2:T :subst0 (s k i0) v0 t1 t2 ⇒
the thesis becomes ∀c:C.∀d:C.∀H6:(getl i0 c (CHead d (Bind Abbr) v0)).∀H7:(sn3 c (THead k u1 t1)).(sn3 d v0)
(H3) by induction hypothesis we know ∀c:C.∀d:C.(getl i0 c (CHead d (Bind Abbr) v0))→(sn3 c u1)→(sn3 d v0)
() by induction hypothesis we know
∀c:C.∀d:C.(getl (s k i0) c (CHead d (Bind Abbr) v0))→(sn3 c t1)→(sn3 d v0)
assume c: C
assume d: C
suppose H6: getl i0 c (CHead d (Bind Abbr) v0)
suppose H7: sn3 c (THead k u1 t1)
(H_y)
by (sn3_gen_head . . . . H7)
sn3 c u1
end of H_y
by (H3 . . H6 H_y)
we proved sn3 d v0
∀c:C.∀d:C.∀H6:(getl i0 c (CHead d (Bind Abbr) v0)).∀H7:(sn3 c (THead k u1 t1)).(sn3 d v0)
∀c:C.∀d:C.(getl i c (CHead d (Bind Abbr) v))→(sn3 c t)→(sn3 d v)
we proved ∀c:C.∀d:C.(getl i c (CHead d (Bind Abbr) v))→(sn3 c t)→(sn3 d v)
we proved
∀v:T
.∀t:T
.∀i:nat
.∀w:T.(ex T λu:T.subst0 i w t u)
→∀c:C.∀d:C.(getl i c (CHead d (Bind Abbr) v))→(sn3 c t)→(sn3 d v)