(* 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_head:
\forall (v: T).(\forall (u1: T).(\forall (u2: T).(\forall (i: nat).((subst1
(subst0_fst v t2 u1 i H0 t1 k)) (\lambda (t3: T).(\lambda (H2: (subst0 (s k
i) v t1 t3)).(subst1_single i v (THead k u1 t1) (THead k t2 t3) (subst0_both
v u1 t2 i H0 k t1 t3 H2)))) t0 H1))))))) u2 H))))).
+(* COMMENTS
+Initial nodes: 369
+END *)
theorem subst1_lift_lt:
\forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst1
nat).(\lambda (H1: (lt i d)).(\lambda (h: nat).(subst1_single i (lift h
(minus d (S i)) u) (lift h d t1) (lift h d t3) (subst0_lift_lt t1 t3 u i H0 d
H1 h))))))) t2 H))))).
+(* COMMENTS
+Initial nodes: 185
+END *)
theorem subst1_lift_ge:
\forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).(\forall
(lift h d t1)))) (\lambda (t3: T).(\lambda (H0: (subst0 i u t1 t3)).(\lambda
(d: nat).(\lambda (H1: (le d i)).(subst1_single (plus i h) u (lift h d t1)
(lift h d t3) (subst0_lift_ge t1 t3 u i h H0 d H1)))))) t2 H)))))).
+(* COMMENTS
+Initial nodes: 157
+END *)
theorem subst1_ex:
\forall (u: T).(\forall (t1: T).(\forall (d: nat).(ex T (\lambda (t2:
d) x0)) (\lambda (t2: T).(subst1 d u (THead k t t0) t2)) (subst1_head u t
(lift (S O) d x) d H2 k t0 (lift (S O) (s k d) x0) H4) (lift (S O) d (THead k
x x0)) (lift_head k x x0 (S O) d))))) H3))))) H1))))))))) t1)).
+(* COMMENTS
+Initial nodes: 925
+END *)
theorem subst1_lift_S:
\forall (u: T).(\forall (i: nat).(\forall (h: nat).((le h i) \to (subst1 i
(S h) (s k i) t0))) (H0 (s k i) h (le_trans h i (s k i) H1 (s_inc k i))) (s k
(S i)) (s_S k i))) (lift (S h) i (THead k t t0)) (lift_head k t t0 (S h) i))
(lift (S h) (S i) (THead k t t0)) (lift_head k t t0 (S h) (S i))))))))))) u).
+(* COMMENTS
+Initial nodes: 1421
+END *)