(* This file was automatically generated: do not edit *********************)
-include "subst1/defs.ma".
+include "LambdaDelta-1/subst1/defs.ma".
-include "subst0/props.ma".
+include "LambdaDelta-1/subst0/props.ma".
theorem subst1_gen_sort:
\forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1
(eq T t (TLRef n)) (land (eq nat n i) (eq T t (lift (S n) O v))))) (or_introl
(eq T (TLRef n) (TLRef n)) (land (eq nat n i) (eq T (TLRef n) (lift (S n) O
v))) (refl_equal T (TLRef n))) (\lambda (t2: T).(\lambda (H0: (subst0 i v
-(TLRef n) t2)).(and_ind (eq nat n i) (eq T t2 (lift (S n) O v)) (or (eq T t2
+(TLRef n) t2)).(land_ind (eq nat n i) (eq T t2 (lift (S n) O v)) (or (eq T t2
(TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v)))) (\lambda (H1: (eq
nat n i)).(\lambda (H2: (eq T t2 (lift (S n) O v))).(or_intror (eq T t2
(TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v))) (conj (eq nat n i)