(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/wcpr0/defs.ma".
+include "Basic-1/wcpr0/defs.ma".
-include "LambdaDelta-1/getl/props.ma".
+include "Basic-1/getl/props.ma".
theorem wcpr0_drop:
\forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to (\forall (h:
T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) x0 x1
(drop_drop (Flat f) n c4 (CHead x0 k0 x1) H6 u2) H7 H8)))))) H5))))))))) k)
h)))))))))) c1 c2 H))).
+(* COMMENTS
+Initial nodes: 1755
+END *)
theorem wcpr0_drop_back:
\forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (h:
T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) x0 x1
(drop_drop (Flat f) n c3 (CHead x0 k0 x1) H6 u1) H7 H8)))))) H5))))))))) k)
h)))))))))) c2 c1 H))).
+(* COMMENTS
+Initial nodes: 1755
+END *)
theorem wcpr0_getl:
\forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to (\forall (h:
(\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
(u3: T).(pr0 u0 u3))) x0 x1 (getl_head (Flat f) n c4 (CHead x0 k0 x1) H6 u2)
H7 H8)))))) H5))))))))) k) h)))))))))) c1 c2 H))).
+(* COMMENTS
+Initial nodes: 2103
+END *)
theorem wcpr0_getl_back:
\forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (h:
(\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
(u3: T).(pr0 u3 u0))) x0 x1 (getl_head (Flat f) n c3 (CHead x0 k0 x1) H6 u1)
H7 H8)))))) H5))))))))) k) h)))))))))) c2 c1 H))).
+(* COMMENTS
+Initial nodes: 2103
+END *)