DEFINITION subst1_subst1()
TYPE =
∀t1:T
.∀t2:T
.∀u2:T
.∀j:nat
.subst1 j u2 t1 t2
→∀u1:T.∀u:T.∀i:nat.(subst1 i u u1 u2)→(ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t t2)
BODY =
assume t1: T
assume t2: T
assume u2: T
assume j: nat
suppose H: subst1 j u2 t1 t2
we proceed by induction on H to prove ∀u1:T.∀u:T.∀i:nat.(subst1 i u u1 u2)→(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t2)
case subst1_refl : ⇒
the thesis becomes ∀u1:T.∀u:T.∀i:nat.(subst1 i u u1 u2)→(ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t t1)
assume u1: T
assume u: T
assume i: nat
suppose : subst1 i u u1 u2
(h1)
by (subst1_refl . . .)
subst1 j u1 t1 t1
end of h1
(h2)
by (subst1_refl . . .)
subst1 (S (plus i j)) u t1 t1
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t t1
∀u1:T.∀u:T.∀i:nat.(subst1 i u u1 u2)→(ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t t1)
case subst1_single : t3:T H0:subst0 j u2 t1 t3 ⇒
the thesis becomes ∀u1:T.∀u:T.∀i:nat.∀H1:(subst1 i u u1 u2).(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t3)
assume u1: T
assume u: T
assume i: nat
suppose H1: subst1 i u u1 u2
assume y: T
suppose H2: subst1 i u u1 y
we proceed by induction on H2 to prove (eq T y u2)→(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t3)
case subst1_refl : ⇒
the thesis becomes (eq T u1 u2)→(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t3)
suppose H3: eq T u1 u2
(h1)
by (subst1_single . . . . H0)
subst1 j u2 t1 t3
end of h1
(h2)
by (subst1_refl . . .)
subst1 (S (plus i j)) u t3 t3
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 T λt:T.subst1 j u2 t1 t λt:T.subst1 (S (plus i j)) u t t3
by (eq_ind_r . . . previous . H3)
we proved ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t3
(eq T u1 u2)→(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t3)
case subst1_single : t0:T H3:subst0 i u u1 t0 ⇒
the thesis becomes ∀H4:(eq T t0 u2).(ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t t3)
suppose H4: eq T t0 u2
(H5)
we proceed by induction on H4 to prove subst0 i u u1 u2
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 i u u1 u2
end of H5
by (subst0_subst0 . . . . H0 . . . H5)
we proved ex2 T λt:T.subst0 j u1 t1 t λt:T.subst0 (S (plus i j)) u t t3
we proceed by induction on the previous result to prove ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t t3
case ex_intro2 : x:T H6:subst0 j u1 t1 x H7:subst0 (S (plus i j)) u x t3 ⇒
the thesis becomes ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t t3
(h1)
by (subst1_single . . . . H6)
subst1 j u1 t1 x
end of h1
(h2)
by (subst1_single . . . . H7)
subst1 (S (plus i j)) u x t3
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t t3
we proved ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t t3
∀H4:(eq T t0 u2).(ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t t3)
we proved (eq T y u2)→(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t3)
we proved ∀y:T.(subst1 i u u1 y)→(eq T y u2)→(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t3)
by (insert_eq . . . . previous H1)
we proved ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t3
∀u1:T.∀u:T.∀i:nat.∀H1:(subst1 i u u1 u2).(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t3)
we proved ∀u1:T.∀u:T.∀i:nat.(subst1 i u u1 u2)→(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t2)
we proved
∀t1:T
.∀t2:T
.∀u2:T
.∀j:nat
.(subst1 j u2 t1 t2)→∀u1:T.∀u:T.∀i:nat.(subst1 i u u1 u2)→(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t0 t2)