(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/subst1/defs.ma".
+include "Basic-1/subst1/defs.ma".
-include "LambdaDelta-1/subst0/props.ma".
+include "Basic-1/subst0/props.ma".
theorem subst1_gen_sort:
\forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1
t (TSort n))) (refl_equal T (TSort n)) (\lambda (t2: T).(\lambda (H0: (subst0
i v (TSort n) t2)).(subst0_gen_sort v t2 i n H0 (eq T t2 (TSort n))))) x
H))))).
+(* COMMENTS
+Initial nodes: 89
+END *)
theorem subst1_gen_lref:
\forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1
(TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v))) (conj (eq nat n i)
(eq T t2 (lift (S n) O v)) H1 H2)))) (subst0_gen_lref v t2 i n H0)))) x
H))))).
+(* COMMENTS
+Initial nodes: 305
+END *)
theorem subst1_gen_head:
\forall (k: K).(\forall (v: T).(\forall (u1: T).(\forall (t1: T).(\forall
i v u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) x0
x1 H2 (subst1_single i v u1 x0 H3) (subst1_single (s k i) v t1 x1 H4)))))))
H1)) (subst0_gen_head k v u1 t1 t2 i H0)))) x H))))))).
+(* COMMENTS
+Initial nodes: 1199
+END *)
theorem subst1_gen_lift_lt:
\forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall
t2 (lift h (S (plus i d)) t3))) (\lambda (t3: T).(subst1 i u t1 t3)) x0 H1
(subst1_single i u t1 x0 H2))))) (subst0_gen_lift_lt u t1 t2 i h d H0)))) x
H))))))).
+(* COMMENTS
+Initial nodes: 395
+END *)
theorem subst1_gen_lift_eq:
\forall (t: T).(\forall (u: T).(\forall (x: T).(\forall (h: nat).(\forall
(\lambda (t0: T).(eq T t0 (lift h d t))) (refl_equal T (lift h d t)) (\lambda
(t2: T).(\lambda (H2: (subst0 i u (lift h d t) t2)).(subst0_gen_lift_false t
u t2 h d i H H0 H2 (eq T t2 (lift h d t))))) x H1))))))))).
+(* COMMENTS
+Initial nodes: 141
+END *)
theorem subst1_gen_lift_ge:
\forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall
T).(eq T t2 (lift h d t3))) (\lambda (t3: T).(subst1 (minus i h) u t1 t3)) x0
H2 (subst1_single (minus i h) u t1 x0 H3))))) (subst0_gen_lift_ge u t1 t2 i h
d H1 H0)))) x H)))))))).
+(* COMMENTS
+Initial nodes: 355
+END *)