(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/subst/fwd.ma".
+include "Basic-1/subst/fwd.ma".
-include "LambdaDelta-1/subst0/defs.ma".
+include "Basic-1/subst0/defs.ma".
-include "LambdaDelta-1/lift/props.ma".
+include "Basic-1/lift/props.ma".
theorem subst_lift_SO:
\forall (v: T).(\forall (t: T).(\forall (d: nat).(eq T (subst d v (lift (S
(THead k (lift (S O) d t0) (lift (S O) (s k d) t1))) (subst_head k v (lift (S
O) d t0) (lift (S O) (s k d) t1) d)) (lift (S O) d (THead k t0 t1))
(lift_head k t0 t1 (S O) d)))))))) t)).
+(* COMMENTS
+Initial nodes: 879
+END *)
theorem subst_subst0:
\forall (v: T).(\forall (t1: T).(\forall (t2: T).(\forall (d: nat).((subst0
(subst (s k i) v0 t3) H3) (subst i v0 u1) H1) (subst i v0 (THead k u2 t4))
(subst_head k v0 u2 t4 i)) (subst i v0 (THead k u1 t3)) (subst_head k v0 u1
t3 i))))))))))))) d v t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 1363
+END *)