DEFINITION sn3_gen_flat()
TYPE =
∀f:F.∀c:C.∀u:T.∀t:T.(sn3 c (THead (Flat f) u t))→(land (sn3 c u) (sn3 c t))
BODY =
assume f: F
assume c: C
assume u: T
assume t: T
suppose H: sn3 c (THead (Flat f) 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 (Flat f) x x0))→(land (sn3 c x) (sn3 c 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 (Flat f) x x0)).(land (sn3 c x) (sn3 c 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 (Flat f) x x0))→(land (sn3 c x) (sn3 c x0)))
assume x: T
assume x0: T
suppose H3: eq T t1 (THead (Flat f) x x0)
(H4)
we proceed by induction on H3 to prove
∀t2:T
.(eq T (THead (Flat f) x x0) t2)→∀P:Prop.P
→(pr3 c (THead (Flat f) x x0) t2
→∀x1:T.∀x2:T.(eq T t2 (THead (Flat f) x1 x2))→(land (sn3 c x1) (sn3 c x2)))
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀t2:T
.(eq T (THead (Flat f) x x0) t2)→∀P:Prop.P
→(pr3 c (THead (Flat f) x x0) t2
→∀x1:T.∀x2:T.(eq T t2 (THead (Flat f) x1 x2))→(land (sn3 c x1) (sn3 c 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 (Flat f) x x0) (THead (Flat f) t2 x0)
assume P: Prop
(H9)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead (Flat f) x x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
<λ:T.T> CASE THead (Flat f) 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 (Flat f) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
THead (Flat f) t2 x0
end of H9
(H11)
consider H9
we proved
eq
T
<λ:T.T> CASE THead (Flat f) x x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
<λ:T.T> CASE THead (Flat f) 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 (Flat f) x x0) (THead (Flat f) t2 x0))→∀P:Prop.P
end of h1
(h2)
by (pr3_refl . .)
we proved pr3 (CHead c (Flat f) t2) x0 x0
by (pr3_head_12 . . . H7 . . . previous)
pr3 c (THead (Flat f) x x0) (THead (Flat f) t2 x0)
end of h2
(h3)
by (refl_equal . .)
eq T (THead (Flat f) t2 x0) (THead (Flat f) t2 x0)
end of h3
by (H4 . h1 h2 . . h3)
land (sn3 c t2) (sn3 c x0)
end of H8
we proceed by induction on H8 to prove sn3 c t2
case conj : H9:sn3 c t2 :sn3 c 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 c x0 t2
(H8)
(h1)
suppose H8: eq T (THead (Flat f) x x0) (THead (Flat f) x t2)
assume P: Prop
(H9)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead (Flat f) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Flat f) 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 (Flat f) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Flat f) x t2
end of H9
(H11)
consider H9
we proved
eq
T
<λ:T.T> CASE THead (Flat f) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Flat f) 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 (Flat f) x x0) (THead (Flat f) x t2))→∀P:Prop.P
end of h1
(h2)
by (pr3_thin_dx . . . H7 . .)
pr3 c (THead (Flat f) x x0) (THead (Flat f) x t2)
end of h2
(h3)
by (refl_equal . .)
eq T (THead (Flat f) x t2) (THead (Flat f) x t2)
end of h3
by (H4 . h1 h2 . . h3)
land (sn3 c x) (sn3 c t2)
end of H8
we proceed by induction on H8 to prove sn3 c t2
case conj : :sn3 c x H10:sn3 c t2 ⇒
the thesis becomes the hypothesis H10
we proved sn3 c t2
we proved ∀t2:T.((eq T x0 t2)→∀P:Prop.P)→(pr3 c x0 t2)→(sn3 c t2)
by (sn3_sing . . previous)
sn3 c x0
end of h2
by (conj . . h1 h2)
we proved land (sn3 c x) (sn3 c x0)
∀x:T.∀x0:T.∀H3:(eq T t1 (THead (Flat f) x x0)).(land (sn3 c x) (sn3 c x0))
we proved ∀x:T.∀x0:T.(eq T y (THead (Flat f) x x0))→(land (sn3 c x) (sn3 c x0))
by (unintro . . . previous)
we proved ∀x:T.(eq T y (THead (Flat f) u x))→(land (sn3 c u) (sn3 c x))
by (unintro . . . previous)
we proved (eq T y (THead (Flat f) u t))→(land (sn3 c u) (sn3 c t))
we proved
∀y:T
.sn3 c y
→(eq T y (THead (Flat f) u t))→(land (sn3 c u) (sn3 c t))
by (insert_eq . . . . previous H)
we proved land (sn3 c u) (sn3 c t)
we proved ∀f:F.∀c:C.∀u:T.∀t:T.(sn3 c (THead (Flat f) u t))→(land (sn3 c u) (sn3 c t))