DEFINITION sn3_bind()
TYPE =
∀b:B
.∀c:C
.∀u:T
.sn3 c u
→∀t:T.(sn3 (CHead c (Bind b) u) t)→(sn3 c (THead (Bind b) u t))
BODY =
assume b: B
assume c: C
assume u: T
suppose H: sn3 c u
we proceed by induction on H to prove ∀t0:T.(sn3 (CHead c (Bind b) u) t0)→(sn3 c (THead (Bind b) u t0))
case sn3_sing : t1:T :∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2) ⇒
the thesis becomes ∀t:T.∀H2:(sn3 (CHead c (Bind b) t1) t).(sn3 c (THead (Bind b) t1 t))
(H1) by induction hypothesis we know
∀t2:T
.(eq T t1 t2)→∀P:Prop.P
→(pr3 c t1 t2
→∀t:T.(sn3 (CHead c (Bind b) t2) t)→(sn3 c (THead (Bind b) t2 t)))
assume t: T
suppose H2: sn3 (CHead c (Bind b) t1) t
we proceed by induction on H2 to prove sn3 c (THead (Bind b) t1 t)
case sn3_sing : t2:T H3:∀t3:T.((eq T t2 t3)→∀P:Prop.P)→(pr3 (CHead c (Bind b) t1) t2 t3)→(sn3 (CHead c (Bind b) t1) t3) ⇒
the thesis becomes sn3 c (THead (Bind b) t1 t2)
(H4) by induction hypothesis we know
∀t3:T
.(eq T t2 t3)→∀P:Prop.P
→(pr3 (CHead c (Bind b) t1) t2 t3)→(sn3 c (THead (Bind b) t1 t3))
assume t3: T
suppose H5: (eq T (THead (Bind b) t1 t2) t3)→∀P:Prop.P
suppose H6: pr3 c (THead (Bind b) t1 t2) t3
(H_x)
by (bind_dec_not . .)
or (eq B b Abst) (not (eq B b Abst))
end of H_x
(H7) consider H_x
we proceed by induction on H7 to prove sn3 c t3
case or_introl : H8:eq B b Abst ⇒
the thesis becomes sn3 c t3
(H9)
we proceed by induction on H8 to prove pr3 c (THead (Bind Abst) t1 t2) t3
case refl_equal : ⇒
the thesis becomes the hypothesis H6
pr3 c (THead (Bind Abst) t1 t2) t3
end of H9
(H10)
we proceed by induction on H8 to prove (eq T (THead (Bind Abst) t1 t2) t3)→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H5
(eq T (THead (Bind Abst) t1 t2) t3)→∀P:Prop.P
end of H10
(H11)
we proceed by induction on H8 to prove
∀t4:T
.(eq T t2 t4)→∀P:Prop.P
→(pr3 (CHead c (Bind Abst) t1) t2 t4)→(sn3 c (THead (Bind Abst) t1 t4))
case refl_equal : ⇒
the thesis becomes the hypothesis H4
∀t4:T
.(eq T t2 t4)→∀P:Prop.P
→(pr3 (CHead c (Bind Abst) t1) t2 t4)→(sn3 c (THead (Bind Abst) t1 t4))
end of H11
(H12)
we proceed by induction on H8 to prove
∀t4:T
.(eq T t2 t4)→∀P:Prop.P
→(pr3 (CHead c (Bind Abst) t1) t2 t4)→(sn3 (CHead c (Bind Abst) t1) t4)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀t4:T
.(eq T t2 t4)→∀P:Prop.P
→(pr3 (CHead c (Bind Abst) t1) t2 t4)→(sn3 (CHead c (Bind Abst) t1) t4)
end of H12
(H13)
we proceed by induction on H8 to prove
∀t4:T
.(eq T t1 t4)→∀P:Prop.P
→(pr3 c t1 t4
→∀t0:T.(sn3 (CHead c (Bind Abst) t4) t0)→(sn3 c (THead (Bind Abst) t4 t0)))
case refl_equal : ⇒
the thesis becomes the hypothesis H1
∀t4:T
.(eq T t1 t4)→∀P:Prop.P
→(pr3 c t1 t4
→∀t0:T.(sn3 (CHead c (Bind Abst) t4) t0)→(sn3 c (THead (Bind Abst) t4 t0)))
end of H13
(H14)
by (pr3_gen_abst . . . . H9)
ex3_2
T
T
λu2:T.λt2:T.eq T t3 (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c t1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 t2)
end of H14
we proceed by induction on H14 to prove sn3 c t3
case ex3_2_intro : x0:T x1:T H15:eq T t3 (THead (Bind Abst) x0 x1) H16:pr3 c t1 x0 H17:∀b0:B.∀u0:T.(pr3 (CHead c (Bind b0) u0) t2 x1) ⇒
the thesis becomes sn3 c t3
(H18)
we proceed by induction on H15 to prove
(eq T (THead (Bind Abst) t1 t2) (THead (Bind Abst) x0 x1))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H10
(eq T (THead (Bind Abst) t1 t2) (THead (Bind Abst) x0 x1))→∀P:Prop.P
end of H18
(H_x0)
by (term_dec . .)
or (eq T t1 x0) (eq T t1 x0)→∀P:Prop.P
end of H_x0
(H19) consider H_x0
we proceed by induction on H19 to prove sn3 c (THead (Bind Abst) x0 x1)
case or_introl : H20:eq T t1 x0 ⇒
the thesis becomes sn3 c (THead (Bind Abst) x0 x1)
(H21)
by (eq_ind_r . . . H18 . H20)
(eq T (THead (Bind Abst) t1 t2) (THead (Bind Abst) t1 x1))→∀P:Prop.P
end of H21
we proceed by induction on H20 to prove sn3 c (THead (Bind Abst) x0 x1)
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Bind Abst) t1 x1)
(H_x1)
by (term_dec . .)
or (eq T t2 x1) (eq T t2 x1)→∀P:Prop.P
end of H_x1
(H23) consider H_x1
we proceed by induction on H23 to prove sn3 c (THead (Bind Abst) t1 x1)
case or_introl : H24:eq T t2 x1 ⇒
the thesis becomes sn3 c (THead (Bind Abst) t1 x1)
(H25)
by (eq_ind_r . . . H21 . H24)
(eq T (THead (Bind Abst) t1 t2) (THead (Bind Abst) t1 t2))→∀P:Prop.P
end of H25
we proceed by induction on H24 to prove sn3 c (THead (Bind Abst) t1 x1)
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Bind Abst) t1 t2)
by (refl_equal . .)
we proved eq T (THead (Bind Abst) t1 t2) (THead (Bind Abst) t1 t2)
by (H25 previous .)
sn3 c (THead (Bind Abst) t1 t2)
sn3 c (THead (Bind Abst) t1 x1)
case or_intror : H24:(eq T t2 x1)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Bind Abst) t1 x1)
by (H17 . .)
we proved pr3 (CHead c (Bind Abst) t1) t2 x1
by (H11 . H24 previous)
sn3 c (THead (Bind Abst) t1 x1)
sn3 c (THead (Bind Abst) t1 x1)
sn3 c (THead (Bind Abst) x0 x1)
case or_intror : H20:(eq T t1 x0)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Bind Abst) x0 x1)
(H_x1)
by (term_dec . .)
or (eq T t2 x1) (eq T t2 x1)→∀P:Prop.P
end of H_x1
(H21) consider H_x1
we proceed by induction on H21 to prove sn3 c (THead (Bind Abst) x0 x1)
case or_introl : H22:eq T t2 x1 ⇒
the thesis becomes sn3 c (THead (Bind Abst) x0 x1)
we proceed by induction on H22 to prove sn3 c (THead (Bind Abst) x0 x1)
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Bind Abst) x0 t2)
by (sn3_sing . . H12)
we proved sn3 (CHead c (Bind Abst) t1) t2
by (sn3_cpr3_trans . . . H16 . . previous)
we proved sn3 (CHead c (Bind Abst) x0) t2
by (H13 . H20 H16 . previous)
sn3 c (THead (Bind Abst) x0 t2)
sn3 c (THead (Bind Abst) x0 x1)
case or_intror : H22:(eq T t2 x1)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Bind Abst) x0 x1)
by (H17 . .)
we proved pr3 (CHead c (Bind Abst) t1) t2 x1
by (H12 . H22 previous)
we proved sn3 (CHead c (Bind Abst) t1) x1
by (sn3_cpr3_trans . . . H16 . . previous)
we proved sn3 (CHead c (Bind Abst) x0) x1
by (H13 . H20 H16 . previous)
sn3 c (THead (Bind Abst) x0 x1)
sn3 c (THead (Bind Abst) x0 x1)
we proved sn3 c (THead (Bind Abst) x0 x1)
by (eq_ind_r . . . previous . H15)
sn3 c t3
sn3 c t3
case or_intror : H8:not (eq B b Abst) ⇒
the thesis becomes sn3 c t3
(H_x0)
by (pr3_gen_bind . H8 . . . . H6)
or
ex3_2
T
T
λu2:T.λt2:T.eq T t3 (THead (Bind b) u2 t2)
λu2:T.λ:T.pr3 c t1 u2
λ:T.λt2:T.pr3 (CHead c (Bind b) t1) t2 t2
pr3 (CHead c (Bind b) t1) t2 (lift (S O) O t3)
end of H_x0
(H9) consider H_x0
we proceed by induction on H9 to prove sn3 c t3
case or_introl : H10:ex3_2 T T λu2:T.λt4:T.eq T t3 (THead (Bind b) u2 t4) λu2:T.λ:T.pr3 c t1 u2 λ:T.λt4:T.pr3 (CHead c (Bind b) t1) t2 t4 ⇒
the thesis becomes sn3 c t3
we proceed by induction on H10 to prove sn3 c t3
case ex3_2_intro : x0:T x1:T H11:eq T t3 (THead (Bind b) x0 x1) H12:pr3 c t1 x0 H13:pr3 (CHead c (Bind b) t1) t2 x1 ⇒
the thesis becomes sn3 c t3
(H14)
we proceed by induction on H11 to prove (eq T (THead (Bind b) t1 t2) (THead (Bind b) x0 x1))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H5
(eq T (THead (Bind b) t1 t2) (THead (Bind b) x0 x1))→∀P:Prop.P
end of H14
(H_x1)
by (term_dec . .)
or (eq T t1 x0) (eq T t1 x0)→∀P:Prop.P
end of H_x1
(H15) consider H_x1
we proceed by induction on H15 to prove sn3 c (THead (Bind b) x0 x1)
case or_introl : H16:eq T t1 x0 ⇒
the thesis becomes sn3 c (THead (Bind b) x0 x1)
(H17)
by (eq_ind_r . . . H14 . H16)
(eq T (THead (Bind b) t1 t2) (THead (Bind b) t1 x1))→∀P:Prop.P
end of H17
we proceed by induction on H16 to prove sn3 c (THead (Bind b) x0 x1)
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Bind b) t1 x1)
(H_x2)
by (term_dec . .)
or (eq T t2 x1) (eq T t2 x1)→∀P:Prop.P
end of H_x2
(H19) consider H_x2
we proceed by induction on H19 to prove sn3 c (THead (Bind b) t1 x1)
case or_introl : H20:eq T t2 x1 ⇒
the thesis becomes sn3 c (THead (Bind b) t1 x1)
(H21)
by (eq_ind_r . . . H17 . H20)
(eq T (THead (Bind b) t1 t2) (THead (Bind b) t1 t2))→∀P:Prop.P
end of H21
we proceed by induction on H20 to prove sn3 c (THead (Bind b) t1 x1)
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Bind b) t1 t2)
by (refl_equal . .)
we proved eq T (THead (Bind b) t1 t2) (THead (Bind b) t1 t2)
by (H21 previous .)
sn3 c (THead (Bind b) t1 t2)
sn3 c (THead (Bind b) t1 x1)
case or_intror : H20:(eq T t2 x1)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Bind b) t1 x1)
by (H4 . H20 H13)
sn3 c (THead (Bind b) t1 x1)
sn3 c (THead (Bind b) t1 x1)
sn3 c (THead (Bind b) x0 x1)
case or_intror : H16:(eq T t1 x0)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Bind b) x0 x1)
(H_x2)
by (term_dec . .)
or (eq T t2 x1) (eq T t2 x1)→∀P:Prop.P
end of H_x2
(H17) consider H_x2
we proceed by induction on H17 to prove sn3 c (THead (Bind b) x0 x1)
case or_introl : H18:eq T t2 x1 ⇒
the thesis becomes sn3 c (THead (Bind b) x0 x1)
we proceed by induction on H18 to prove sn3 c (THead (Bind b) x0 x1)
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Bind b) x0 t2)
by (sn3_sing . . H3)
we proved sn3 (CHead c (Bind b) t1) t2
by (sn3_cpr3_trans . . . H12 . . previous)
we proved sn3 (CHead c (Bind b) x0) t2
by (H1 . H16 H12 . previous)
sn3 c (THead (Bind b) x0 t2)
sn3 c (THead (Bind b) x0 x1)
case or_intror : H18:(eq T t2 x1)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Bind b) x0 x1)
by (H3 . H18 H13)
we proved sn3 (CHead c (Bind b) t1) x1
by (sn3_cpr3_trans . . . H12 . . previous)
we proved sn3 (CHead c (Bind b) x0) x1
by (H1 . H16 H12 . previous)
sn3 c (THead (Bind b) x0 x1)
sn3 c (THead (Bind b) x0 x1)
we proved sn3 c (THead (Bind b) x0 x1)
by (eq_ind_r . . . previous . H11)
sn3 c t3
sn3 c t3
case or_intror : H10:pr3 (CHead c (Bind b) t1) t2 (lift (S O) O t3) ⇒
the thesis becomes sn3 c t3
(h1)
by (sn3_sing . . H3)
we proved sn3 (CHead c (Bind b) t1) t2
by (sn3_pr3_trans . . previous . H10)
sn3 (CHead c (Bind b) t1) (lift (S O) O t3)
end of h1
(h2)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
drop (S O) O (CHead c (Bind b) t1) c
end of h2
by (sn3_gen_lift . . . . h1 . h2)
sn3 c t3
sn3 c t3
we proved sn3 c t3
we proved
∀t3:T
.(eq T (THead (Bind b) t1 t2) t3)→∀P:Prop.P
→(pr3 c (THead (Bind b) t1 t2) t3)→(sn3 c t3)
by (sn3_sing . . previous)
sn3 c (THead (Bind b) t1 t2)
we proved sn3 c (THead (Bind b) t1 t)
∀t:T.∀H2:(sn3 (CHead c (Bind b) t1) t).(sn3 c (THead (Bind b) t1 t))
we proved ∀t0:T.(sn3 (CHead c (Bind b) u) t0)→(sn3 c (THead (Bind b) u t0))
we proved
∀b:B
.∀c:C
.∀u:T
.sn3 c u
→∀t0:T.(sn3 (CHead c (Bind b) u) t0)→(sn3 c (THead (Bind b) u t0))