(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/pr0/props.ma".
+include "Basic-1/pr0/props.ma".
-include "LambdaDelta-1/subst1/defs.ma".
+include "Basic-1/subst1/defs.ma".
theorem pr0_delta1:
\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (t1: T).(\forall
Abbr) u1 t1) (THead (Bind Abbr) u2 t))) (pr0_comp u1 u2 H t1 t2 H0 (Bind
Abbr)) (\lambda (t0: T).(\lambda (H2: (subst0 O u2 t2 t0)).(pr0_delta u1 u2 H
t1 t2 H0 t0 H2))) w H1)))))))).
+(* COMMENTS
+Initial nodes: 115
+END *)
theorem pr0_subst1_back:
\forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst1
(H2: (subst0 i u1 t1 x)).(\lambda (H3: (pr0 x t0)).(ex_intro2 T (\lambda (t:
T).(subst1 i u1 t1 t)) (\lambda (t: T).(pr0 t t0)) x (subst1_single i u1 t1 x
H2) H3)))) (pr0_subst0_back u2 t1 t0 i H0 u1 H1)))))) t2 H))))).
+(* COMMENTS
+Initial nodes: 251
+END *)
theorem pr0_subst1_fwd:
\forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst1
(H2: (subst0 i u1 t1 x)).(\lambda (H3: (pr0 t0 x)).(ex_intro2 T (\lambda (t:
T).(subst1 i u1 t1 t)) (\lambda (t: T).(pr0 t0 t)) x (subst1_single i u1 t1 x
H2) H3)))) (pr0_subst0_fwd u2 t1 t0 i H0 u1 H1)))))) t2 H))))).
+(* COMMENTS
+Initial nodes: 251
+END *)
theorem pr0_subst1:
\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (v1: T).(\forall
(pr0 t0 x)).(\lambda (H5: (subst0 i v2 t2 x)).(ex_intro2 T (\lambda (w2:
T).(pr0 t0 w2)) (\lambda (w2: T).(subst1 i v2 t2 w2)) x H4 (subst1_single i
v2 t2 x H5))))) H3)) (pr0_subst0 t1 t2 H v1 t0 i H1 v2 H2)))))) w1 H0))))))).
+(* COMMENTS
+Initial nodes: 385
+END *)