DEFINITION subst1_confluence_neq()
TYPE =
∀t0:T
.∀t1:T
.∀u1:T
.∀i1:nat
.subst1 i1 u1 t0 t1
→∀t2:T.∀u2:T.∀i2:nat.(subst1 i2 u2 t0 t2)→(not (eq nat i1 i2))→(ex2 T λt:T.subst1 i2 u2 t1 t λt:T.subst1 i1 u1 t2 t)
BODY =
assume t0: T
assume t1: T
assume u1: T
assume i1: nat
suppose H: subst1 i1 u1 t0 t1
we proceed by induction on H to prove ∀t2:T.∀u2:T.∀i2:nat.(subst1 i2 u2 t0 t2)→(not (eq nat i1 i2))→(ex2 T λt3:T.subst1 i2 u2 t1 t3 λt3:T.subst1 i1 u1 t2 t3)
case subst1_refl : ⇒
the thesis becomes ∀t2:T.∀u2:T.∀i2:nat.(subst1 i2 u2 t0 t2)→(not (eq nat i1 i2))→(ex2 T λt:T.subst1 i2 u2 t0 t λt:T.subst1 i1 u1 t2 t)
assume t2: T
assume u2: T
assume i2: nat
suppose H0: subst1 i2 u2 t0 t2
suppose : not (eq nat i1 i2)
by (subst1_refl . . .)
we proved subst1 i1 u1 t2 t2
by (ex_intro2 . . . . H0 previous)
we proved ex2 T λt:T.subst1 i2 u2 t0 t λt:T.subst1 i1 u1 t2 t
∀t2:T.∀u2:T.∀i2:nat.(subst1 i2 u2 t0 t2)→(not (eq nat i1 i2))→(ex2 T λt:T.subst1 i2 u2 t0 t λt:T.subst1 i1 u1 t2 t)
case subst1_single : t2:T H0:subst0 i1 u1 t0 t2 ⇒
the thesis becomes ∀t3:T.∀u2:T.∀i2:nat.∀H1:(subst1 i2 u2 t0 t3).∀H2:(not (eq nat i1 i2)).(ex2 T λt4:T.subst1 i2 u2 t2 t4 λt4:T.subst1 i1 u1 t3 t4)
assume t3: T
assume u2: T
assume i2: nat
suppose H1: subst1 i2 u2 t0 t3
suppose H2: not (eq nat i1 i2)
we proceed by induction on H1 to prove ex2 T λt4:T.subst1 i2 u2 t2 t4 λt4:T.subst1 i1 u1 t3 t4
case subst1_refl : ⇒
the thesis becomes ex2 T λt:T.subst1 i2 u2 t2 t λt:T.subst1 i1 u1 t0 t
(h1)
by (subst1_refl . . .)
subst1 i2 u2 t2 t2
end of h1
(h2)
by (subst1_single . . . . H0)
subst1 i1 u1 t0 t2
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst1 i2 u2 t2 t λt:T.subst1 i1 u1 t0 t
case subst1_single : t4:T H3:subst0 i2 u2 t0 t4 ⇒
the thesis becomes ex2 T λt:T.subst1 i2 u2 t2 t λt:T.subst1 i1 u1 t4 t
by (sym_not_eq . . . H2)
we proved not (eq nat i2 i1)
by (subst0_confluence_neq . . . . H3 . . . H0 previous)
we proved ex2 T λt:T.subst0 i1 u1 t4 t λt:T.subst0 i2 u2 t2 t
we proceed by induction on the previous result to prove ex2 T λt:T.subst1 i2 u2 t2 t λt:T.subst1 i1 u1 t4 t
case ex_intro2 : x:T H4:subst0 i1 u1 t4 x H5:subst0 i2 u2 t2 x ⇒
the thesis becomes ex2 T λt:T.subst1 i2 u2 t2 t λt:T.subst1 i1 u1 t4 t
(h1)
by (subst1_single . . . . H5)
subst1 i2 u2 t2 x
end of h1
(h2)
by (subst1_single . . . . H4)
subst1 i1 u1 t4 x
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst1 i2 u2 t2 t λt:T.subst1 i1 u1 t4 t
ex2 T λt:T.subst1 i2 u2 t2 t λt:T.subst1 i1 u1 t4 t
we proved ex2 T λt4:T.subst1 i2 u2 t2 t4 λt4:T.subst1 i1 u1 t3 t4
∀t3:T.∀u2:T.∀i2:nat.∀H1:(subst1 i2 u2 t0 t3).∀H2:(not (eq nat i1 i2)).(ex2 T λt4:T.subst1 i2 u2 t2 t4 λt4:T.subst1 i1 u1 t3 t4)
we proved ∀t2:T.∀u2:T.∀i2:nat.(subst1 i2 u2 t0 t2)→(not (eq nat i1 i2))→(ex2 T λt3:T.subst1 i2 u2 t1 t3 λt3:T.subst1 i1 u1 t2 t3)
we proved
∀t0:T
.∀t1:T
.∀u1:T
.∀i1:nat.(subst1 i1 u1 t0 t1)→∀t2:T.∀u2:T.∀i2:nat.(subst1 i2 u2 t0 t2)→(not (eq nat i1 i2))→(ex2 T λt3:T.subst1 i2 u2 t1 t3 λt3:T.subst1 i1 u1 t2 t3)