INDUCTIVE DEFINITION subst0 () [ ]
OF ARITY nat→T→T→T→Prop
BUILT FROM:
     subst0_lref: ∀v:T.∀i:nat.(subst0 i v (TLRef i) (lift (S i) O v))
   | subst0_fst: ∀v:T.∀u2:T.∀u1:T.∀i:nat.(subst0 i v u1 u2)→∀t:T.∀k:K.(subst0 i v (THead k u1 t) (THead k u2 t))
   | subst0_snd: ∀k:K.∀v:T.∀t2:T.∀t1:T.∀i:nat.(subst0 (s k i) v t1 t2)→∀u:T.(subst0 i v (THead k u t1) (THead k u t2))
   | subst0_both: ∀v:T
                             .∀u1:T
                               .∀u2:T
                                 .∀i:nat
                                   .(subst0 i v u1 u2)→∀k:K.∀t1:T.∀t2:T.(subst0 (s k i) v t1 t2)→(subst0 i v (THead k u1 t1) (THead k u2 t2))