DEFINITION subst1_confluence_lift()
TYPE =
∀t0:T
.∀t1:T
.∀u:T
.∀i:nat
.(subst1 i u t0 (lift (S O) i t1))→∀t2:T.(subst1 i u t0 (lift (S O) i t2))→(eq T t1 t2)
BODY =
assume t0: T
assume t1: T
assume u: T
assume i: nat
suppose H: subst1 i u t0 (lift (S O) i t1)
assume y: T
suppose H0: subst1 i u t0 y
we proceed by induction on H0 to prove
(eq T y (lift (S O) i t1))→∀t2:T.(subst1 i u t0 (lift (S O) i t2))→(eq T t1 t2)
case subst1_refl : ⇒
the thesis becomes (eq T t0 (lift (S O) i t1))→∀t2:T.(subst1 i u t0 (lift (S O) i t2))→(eq T t1 t2)
suppose H1: eq T t0 (lift (S O) i t1)
assume t2: T
suppose H2: subst1 i u t0 (lift (S O) i t2)
(H3)
we proceed by induction on H1 to prove subst1 i u (lift (S O) i t1) (lift (S O) i t2)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
subst1 i u (lift (S O) i t1) (lift (S O) i t2)
end of H3
(H4)
(h1) by (le_n .) we proved le i i
(h2)
(h1)
by (le_n .)
we proved le (plus (S O) i) (plus (S O) i)
lt i (plus (S O) i)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus i (S O)) (plus (S O) i)
end of h2
by (eq_ind_r . . . h1 . h2)
lt i (plus i (S O))
end of h2
by (subst1_gen_lift_eq . . . . . . h1 h2 H3)
we proved eq T (lift (S O) i t2) (lift (S O) i t1)
by (sym_eq . . . previous)
eq T (lift (S O) i t1) (lift (S O) i t2)
end of H4
by (lift_inj . . . . H4)
we proved eq T t1 t2
(eq T t0 (lift (S O) i t1))→∀t2:T.(subst1 i u t0 (lift (S O) i t2))→(eq T t1 t2)
case subst1_single : t2:T H1:subst0 i u t0 t2 ⇒
the thesis becomes ∀H2:(eq T t2 (lift (S O) i t1)).∀t3:T.∀H3:(subst1 i u t0 (lift (S O) i t3)).(eq T t1 t3)
suppose H2: eq T t2 (lift (S O) i t1)
assume t3: T
suppose H3: subst1 i u t0 (lift (S O) i t3)
(H4)
we proceed by induction on H2 to prove subst0 i u t0 (lift (S O) i t1)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
subst0 i u t0 (lift (S O) i t1)
end of H4
assume y0: T
suppose H5: subst1 i u t0 y0
we proceed by induction on H5 to prove (eq T y0 (lift (S O) i t3))→(eq T t1 t3)
case subst1_refl : ⇒
the thesis becomes (eq T t0 (lift (S O) i t3))→(eq T t1 t3)
suppose H6: eq T t0 (lift (S O) i t3)
(H7)
we proceed by induction on H6 to prove subst0 i u (lift (S O) i t3) (lift (S O) i t1)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
subst0 i u (lift (S O) i t3) (lift (S O) i t1)
end of H7
(h1) by (le_n .) we proved le i i
(h2)
(h1)
by (le_n .)
we proved le (plus (S O) i) (plus (S O) i)
lt i (plus (S O) i)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus i (S O)) (plus (S O) i)
end of h2
by (eq_ind_r . . . h1 . h2)
lt i (plus i (S O))
end of h2
by (subst0_gen_lift_false . . . . . . h1 h2 H7 .)
we proved eq T t1 t3
(eq T t0 (lift (S O) i t3))→(eq T t1 t3)
case subst1_single : t4:T H6:subst0 i u t0 t4 ⇒
the thesis becomes ∀H7:(eq T t4 (lift (S O) i t3)).(eq T t1 t3)
suppose H7: eq T t4 (lift (S O) i t3)
(H8)
we proceed by induction on H7 to prove subst0 i u t0 (lift (S O) i t3)
case refl_equal : ⇒
the thesis becomes the hypothesis H6
subst0 i u t0 (lift (S O) i t3)
end of H8
by (subst0_confluence_lift . . . . H8 . H4)
we proved eq T t3 t1
by (sym_eq . . . previous)
we proved eq T t1 t3
∀H7:(eq T t4 (lift (S O) i t3)).(eq T t1 t3)
we proved (eq T y0 (lift (S O) i t3))→(eq T t1 t3)
we proved ∀y0:T.(subst1 i u t0 y0)→(eq T y0 (lift (S O) i t3))→(eq T t1 t3)
by (insert_eq . . . . previous H3)
we proved eq T t1 t3
∀H2:(eq T t2 (lift (S O) i t1)).∀t3:T.∀H3:(subst1 i u t0 (lift (S O) i t3)).(eq T t1 t3)
we proved
(eq T y (lift (S O) i t1))→∀t2:T.(subst1 i u t0 (lift (S O) i t2))→(eq T t1 t2)
we proved
∀y:T
.subst1 i u t0 y
→(eq T y (lift (S O) i t1))→∀t2:T.(subst1 i u t0 (lift (S O) i t2))→(eq T t1 t2)
by (insert_eq . . . . previous H)
we proved ∀t2:T.(subst1 i u t0 (lift (S O) i t2))→(eq T t1 t2)
we proved
∀t0:T
.∀t1:T
.∀u:T
.∀i:nat
.(subst1 i u t0 (lift (S O) i t1))→∀t2:T.(subst1 i u t0 (lift (S O) i t2))→(eq T t1 t2)