+implied lemma subst1_ind:
+ \forall (i: nat).(\forall (v: T).(\forall (t1: T).(\forall (P: ((T \to
+Prop))).((P t1) \to (((\forall (t2: T).((subst0 i v t1 t2) \to (P t2)))) \to
+(\forall (t: T).((subst1 i v t1 t) \to (P t))))))))
+\def
+ \lambda (i: nat).(\lambda (v: T).(\lambda (t1: T).(\lambda (P: ((T \to
+Prop))).(\lambda (f: (P t1)).(\lambda (f0: ((\forall (t2: T).((subst0 i v t1
+t2) \to (P t2))))).(\lambda (t: T).(\lambda (s0: (subst1 i v t1 t)).(match s0
+with [subst1_refl \Rightarrow f | (subst1_single x x0) \Rightarrow (f0 x
+x0)])))))))).
+
+lemma subst1_gen_sort: