(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/subst0/props.ma".
+include "Basic-1/subst0/props.ma".
theorem subst0_subst0:
\forall (t1: T).(\forall (t2: T).(\forall (u2: T).(\forall (j: nat).((subst0
t (THead k u0 t3))) (THead k x0 x) (subst0_both u3 u1 x0 i H7 k t0 x H5)
(subst0_both u x0 u0 (S (plus i0 i)) H8 k x t3 H10))))))) (H1 u3 u i0 H4)))))
(H3 u3 u i0 H4))))))))))))))))) j u2 t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 1613
+END *)
theorem subst0_subst0_back:
\forall (t1: T).(\forall (t2: T).(\forall (u2: T).(\forall (j: nat).((subst0
x) (subst0_both u3 u1 x0 i H7 k t0 x H5) (subst0_both u u0 x0 (S (plus i0 i))
H8 k t3 x H10))))))) (H1 u3 u i0 H4))))) (H3 u3 u i0 H4))))))))))))))))) j u2
t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 1613
+END *)
theorem subst0_trans:
\forall (t2: T).(\forall (t1: T).(\forall (v: T).(\forall (i: nat).((subst0
T).(subst0 i0 v0 (THead k u1 t0) t)) (subst0_both v0 u1 x0 i0 (H1 x0 H7) k t0
x1 (H3 x1 H8)) t4 H6)))))) H5)) (subst0_gen_head k v0 u2 t3 t4 i0
H4))))))))))))))) i v t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 2555
+END *)
theorem subst0_confluence_neq:
\forall (t0: T).(\forall (t1: T).(\forall (u1: T).(\forall (i1:
(H12: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 H12)))))))))) (H1 x0 u3 i2
H8 H5)) t4 H7)))))) H6)) (subst0_gen_head k u3 u0 t2 t4 i2
H4)))))))))))))))))) i1 u1 t0 t1 H))))).
+(* COMMENTS
+Initial nodes: 5375
+END *)
theorem subst0_confluence_eq:
\forall (t0: T).(\forall (t1: T).(\forall (u: T).(\forall (i: nat).((subst0
k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3)) (subst0_both v x0 u2
i0 H10 k x1 t3 H9))) (H1 x0 H7))) (H3 x1 H8)) t4 H6)))))) H5))
(subst0_gen_head k v u1 t2 t4 i0 H4))))))))))))))) i u t0 t1 H))))).
+(* COMMENTS
+Initial nodes: 25595
+END *)
theorem subst0_confluence_lift:
\forall (t0: T).(\forall (t1: T).(\forall (u: T).(\forall (i: nat).((subst0
(eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O)
i)) (plus i (S O)) (plus_sym i (S O))) H1 (eq T t1 t2)))
(subst0_confluence_eq t0 (lift (S O) i t2) u i H0 (lift (S O) i t1) H)))))))).
+(* COMMENTS
+Initial nodes: 703
+END *)