INDUCTIVE DEFINITION subst1 () [ :nat, :T, :T ]
OF ARITY T→Prop
BUILT FROM:
     subst1_refl: subst1 i v t1 t1
   | subst1_single: ∀t2:T.(subst0 i v t1 t2)→(subst1 i v t1 t2)