DEFINITION sn3_gen_bind()
TYPE =
∀b:B
.∀c:C
.∀u:T
.∀t:T
.sn3 c (THead (Bind b) u t)
→land (sn3 c u) (sn3 (CHead c (Bind b) u) t)
BODY =
assume b: B
assume c: C
assume u: T
assume t: T
suppose H: sn3 c (THead (Bind b) u t)
assume y: T
suppose H0: sn3 c y
we proceed by induction on H0 to prove
∀x:T
.∀x0:T
.eq T y (THead (Bind b) x x0)
→land (sn3 c x) (sn3 (CHead c (Bind b) x) x0)
case sn3_sing : t1:T H1:∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2) ⇒
the thesis becomes
∀x:T
.∀x0:T
.∀H3:eq T t1 (THead (Bind b) x x0)
.land (sn3 c x) (sn3 (CHead c (Bind b) x) x0)
(H2) by induction hypothesis we know
∀t2:T
.(eq T t1 t2)→∀P:Prop.P
→(pr3 c t1 t2
→∀x:T
.∀x0:T
.eq T t2 (THead (Bind b) x x0)
→land (sn3 c x) (sn3 (CHead c (Bind b) x) x0))
assume x: T
assume x0: T
suppose H3: eq T t1 (THead (Bind b) x x0)
(H4)
we proceed by induction on H3 to prove
∀t2:T
.(eq T (THead (Bind b) x x0) t2)→∀P:Prop.P
→(pr3 c (THead (Bind b) x x0) t2
→∀x1:T
.∀x2:T
.eq T t2 (THead (Bind b) x1 x2)
→land (sn3 c x1) (sn3 (CHead c (Bind b) x1) x2))
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀t2:T
.(eq T (THead (Bind b) x x0) t2)→∀P:Prop.P
→(pr3 c (THead (Bind b) x x0) t2
→∀x1:T
.∀x2:T
.eq T t2 (THead (Bind b) x1 x2)
→land (sn3 c x1) (sn3 (CHead c (Bind b) x1) x2))
end of H4
(h1)
assume t2: T
suppose H6: (eq T x t2)→∀P:Prop.P
suppose H7: pr3 c x t2
(H8)
(h1)
suppose H8: eq T (THead (Bind b) x x0) (THead (Bind b) t2 x0)
assume P: Prop
(H9)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead (Bind b) x x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind b) t2 x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
THead (Bind b) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
THead (Bind b) t2 x0
end of H9
(H11)
consider H9
we proved
eq
T
<λ:T.T> CASE THead (Bind b) x x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind b) t2 x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
that is equivalent to eq T x t2
by (eq_ind_r . . . H6 . previous)
(eq T x x)→∀P0:Prop.P0
end of H11
by (refl_equal . .)
we proved eq T x x
by (H11 previous .)
we proved P
(eq T (THead (Bind b) x x0) (THead (Bind b) t2 x0))→∀P:Prop.P
end of h1
(h2)
by (pr3_refl . .)
we proved pr3 (CHead c (Bind b) t2) x0 x0
by (pr3_head_12 . . . H7 . . . previous)
pr3 c (THead (Bind b) x x0) (THead (Bind b) t2 x0)
end of h2
(h3)
by (refl_equal . .)
eq T (THead (Bind b) t2 x0) (THead (Bind b) t2 x0)
end of h3
by (H4 . h1 h2 . . h3)
land (sn3 c t2) (sn3 (CHead c (Bind b) t2) x0)
end of H8
we proceed by induction on H8 to prove sn3 c t2
case conj : H9:sn3 c t2 :sn3 (CHead c (Bind b) t2) x0 ⇒
the thesis becomes the hypothesis H9
we proved sn3 c t2
we proved ∀t2:T.((eq T x t2)→∀P:Prop.P)→(pr3 c x t2)→(sn3 c t2)
by (sn3_sing . . previous)
sn3 c x
end of h1
(h2)
assume t2: T
suppose H6: (eq T x0 t2)→∀P:Prop.P
suppose H7: pr3 (CHead c (Bind b) x) x0 t2
(H8)
(h1)
suppose H8: eq T (THead (Bind b) x x0) (THead (Bind b) x t2)
assume P: Prop
(H9)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead (Bind b) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind b) x t2 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind b) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind b) x t2
end of H9
(H11)
consider H9
we proved
eq
T
<λ:T.T> CASE THead (Bind b) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind b) x t2 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
that is equivalent to eq T x0 t2
by (eq_ind_r . . . H6 . previous)
(eq T x0 x0)→∀P0:Prop.P0
end of H11
by (refl_equal . .)
we proved eq T x0 x0
by (H11 previous .)
we proved P
(eq T (THead (Bind b) x x0) (THead (Bind b) x t2))→∀P:Prop.P
end of h1
(h2)
by (pr3_refl . .)
we proved pr3 c x x
by (pr3_head_12 . . . previous . . . H7)
pr3 c (THead (Bind b) x x0) (THead (Bind b) x t2)
end of h2
(h3)
by (refl_equal . .)
eq T (THead (Bind b) x t2) (THead (Bind b) x t2)
end of h3
by (H4 . h1 h2 . . h3)
land (sn3 c x) (sn3 (CHead c (Bind b) x) t2)
end of H8
we proceed by induction on H8 to prove sn3 (CHead c (Bind b) x) t2
case conj : :sn3 c x H10:sn3 (CHead c (Bind b) x) t2 ⇒
the thesis becomes the hypothesis H10
we proved sn3 (CHead c (Bind b) x) t2
we proved
∀t2:T
.(eq T x0 t2)→∀P:Prop.P
→(pr3 (CHead c (Bind b) x) x0 t2)→(sn3 (CHead c (Bind b) x) t2)
by (sn3_sing . . previous)
sn3 (CHead c (Bind b) x) x0
end of h2
by (conj . . h1 h2)
we proved land (sn3 c x) (sn3 (CHead c (Bind b) x) x0)
∀x:T
.∀x0:T
.∀H3:eq T t1 (THead (Bind b) x x0)
.land (sn3 c x) (sn3 (CHead c (Bind b) x) x0)
we proved
∀x:T
.∀x0:T
.eq T y (THead (Bind b) x x0)
→land (sn3 c x) (sn3 (CHead c (Bind b) x) x0)
by (unintro . . . previous)
we proved
∀x:T
.eq T y (THead (Bind b) u x)
→land (sn3 c u) (sn3 (CHead c (Bind b) u) x)
by (unintro . . . previous)
we proved
eq T y (THead (Bind b) u t)
→land (sn3 c u) (sn3 (CHead c (Bind b) u) t)
we proved
∀y:T
.sn3 c y
→(eq T y (THead (Bind b) u t)
→land (sn3 c u) (sn3 (CHead c (Bind b) u) t))
by (insert_eq . . . . previous H)
we proved land (sn3 c u) (sn3 (CHead c (Bind b) u) t)
we proved
∀b:B
.∀c:C
.∀u:T
.∀t:T
.sn3 c (THead (Bind b) u t)
→land (sn3 c u) (sn3 (CHead c (Bind b) u) t)