(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/pr0/defs.ma".
+include "Basic-1/pr0/defs.ma".
-include "LambdaDelta-1/subst0/subst0.ma".
+include "Basic-1/subst0/subst0.ma".
theorem pr0_lift:
\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (h: nat).(\forall
t3)) (\lambda (t: T).(pr0 t (lift h d t4))) (pr0_tau (lift h (s (Flat Cast)
d) t3) (lift h d t4) (H1 h d) (lift h d u)) (lift h d (THead (Flat Cast) u
t3)) (lift_head (Flat Cast) u t3 h d))))))))) t1 t2 H))).
+(* COMMENTS
+Initial nodes: 2845
+END *)
theorem pr0_subst0_back:
\forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst0
(t: T).(subst0 i0 u0 (THead k u1 t3) t)) (\lambda (t: T).(pr0 t (THead k u3
t4))) (THead k x0 x) (subst0_both u0 u1 x0 i0 H7 k t3 x H5) (pr0_comp x0 u3
H8 x t4 H6 k))))) (H1 u0 H4))))) (H3 u0 H4))))))))))))))) i u2 t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 979
+END *)
theorem pr0_subst0_fwd:
\forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst0
(t: T).(subst0 i0 u0 (THead k u1 t3) t)) (\lambda (t: T).(pr0 (THead k u3 t4)
t)) (THead k x0 x) (subst0_both u0 u1 x0 i0 H7 k t3 x H5) (pr0_comp u3 x0 H8
t4 x H6 k))))) (H1 u0 H4))))) (H3 u0 H4))))))))))))))) i u2 t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 979
+END *)
theorem pr0_subst0:
\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (v1: T).(\forall
x (pr0_tau x1 x H9 x0) H10))))) H8)) (H1 v1 x1 (s (Flat Cast) i) H7 v2 H3))
w1 H5)))))) H4)) (subst0_gen_head (Flat Cast) v1 u t3 w1 i H2))))))))))))) t1
t2 H))).
+(* COMMENTS
+Initial nodes: 38857
+END *)