DEFINITION subst1_head()
TYPE =
∀v:T
.∀u1:T
.∀u2:T
.∀i:nat
.(subst1 i v u1 u2)→∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u2 t2))
BODY =
assume v: T
assume u1: T
assume u2: T
assume i: nat
suppose H: subst1 i v u1 u2
we proceed by induction on H to prove ∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u2 t2))
case subst1_refl : ⇒
the thesis becomes ∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u1 t2))
assume k: K
assume t1: T
assume t2: T
suppose H0: subst1 (s k i) v t1 t2
we proceed by induction on H0 to prove subst1 i v (THead k u1 t1) (THead k u1 t2)
case subst1_refl : ⇒
the thesis becomes subst1 i v (THead k u1 t1) (THead k u1 t1)
by (subst1_refl . . .)
subst1 i v (THead k u1 t1) (THead k u1 t1)
case subst1_single : t3:T H1:subst0 (s k i) v t1 t3 ⇒
the thesis becomes subst1 i v (THead k u1 t1) (THead k u1 t3)
by (subst0_snd . . . . . H1 .)
we proved subst0 i v (THead k u1 t1) (THead k u1 t3)
by (subst1_single . . . . previous)
subst1 i v (THead k u1 t1) (THead k u1 t3)
we proved subst1 i v (THead k u1 t1) (THead k u1 t2)
∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u1 t2))
case subst1_single : t2:T H0:subst0 i v u1 t2 ⇒
the thesis becomes ∀k:K.∀t1:T.∀t0:T.∀H1:(subst1 (s k i) v t1 t0).(subst1 i v (THead k u1 t1) (THead k t2 t0))
assume k: K
assume t1: T
assume t0: T
suppose H1: subst1 (s k i) v t1 t0
we proceed by induction on H1 to prove subst1 i v (THead k u1 t1) (THead k t2 t0)
case subst1_refl : ⇒
the thesis becomes subst1 i v (THead k u1 t1) (THead k t2 t1)
by (subst0_fst . . . . H0 . .)
we proved subst0 i v (THead k u1 t1) (THead k t2 t1)
by (subst1_single . . . . previous)
subst1 i v (THead k u1 t1) (THead k t2 t1)
case subst1_single : t3:T H2:subst0 (s k i) v t1 t3 ⇒
the thesis becomes subst1 i v (THead k u1 t1) (THead k t2 t3)
by (subst0_both . . . . H0 . . . H2)
we proved subst0 i v (THead k u1 t1) (THead k t2 t3)
by (subst1_single . . . . previous)
subst1 i v (THead k u1 t1) (THead k t2 t3)
we proved subst1 i v (THead k u1 t1) (THead k t2 t0)
∀k:K.∀t1:T.∀t0:T.∀H1:(subst1 (s k i) v t1 t0).(subst1 i v (THead k u1 t1) (THead k t2 t0))
we proved ∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u2 t2))
we proved
∀v:T
.∀u1:T
.∀u2:T
.∀i:nat
.(subst1 i v u1 u2)→∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u2 t2))