(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/pr2/defs.ma".
+include "Basic-1/pr2/defs.ma".
-include "LambdaDelta-1/pr0/subst1.ma".
+include "Basic-1/pr0/subst1.ma".
-include "LambdaDelta-1/pr0/fwd.ma".
+include "Basic-1/pr0/fwd.ma".
-include "LambdaDelta-1/csubst1/getl.ma".
+include "Basic-1/csubst1/getl.ma".
-include "LambdaDelta-1/csubst1/fwd.ma".
+include "Basic-1/csubst1/fwd.ma".
-include "LambdaDelta-1/subst1/subst1.ma".
+include "Basic-1/subst1/subst1.ma".
-include "LambdaDelta-1/getl/drop.ma".
+include "Basic-1/getl/drop.ma".
theorem pr2_delta1:
\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c
t)).(subst1_ind i u t2 (\lambda (t0: T).(pr2 c t1 t0)) (pr2_free c t1 t2 H0)
(\lambda (t0: T).(\lambda (H2: (subst0 i u t2 t0)).(pr2_delta c d u i H t1 t2
H0 t0 H2))) t H1)))))))))).
+(* COMMENTS
+Initial nodes: 111
+END *)
theorem pr2_subst1:
\forall (c: C).(\forall (e: C).(\forall (v: T).(\forall (i: nat).((getl i c
(subst1_confluence_eq t4 t v i (subst1_single i v t4 t H18) x H9)))))))
H14)))))))))) (pr0_subst1 t3 t4 H3 v w1 i H6 v (pr0_refl v))) c0
H5))))))))))))))) y t1 t2 H1))) H0)))))))).
+(* COMMENTS
+Initial nodes: 1311
+END *)
theorem pr2_gen_cabbr:
\forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall
(S O) d0 x0) u0 d0 H11 (sym_not_eq nat d0 i (lt_neq d0 i H12))))))))))
(pr0_gen_lift x1 x (S O) d0 H7))))) (pr0_subst1 t3 t4 H1 u0 (lift (S O) d0
x1) d0 H6 u0 (pr0_refl u0))))))))))))))))))))))) c t1 t2 H)))).
+(* COMMENTS
+Initial nodes: 3757
+END *)