(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/drop1/fwd.ma".
+include "Basic-1/drop1/fwd.ma".
-include "LambdaDelta-1/getl/drop.ma".
+include "Basic-1/getl/drop.ma".
theorem drop1_getl_trans:
\forall (hds: PList).(\forall (c1: C).(\forall (c2: C).((drop1 hds c2 c1)
(ptrans hds0 i) e2 e1)) (\lambda (e2: C).(getl (plus (trans hds0 i) h) c2
(CHead e2 (Bind b) (lift1 (ptrans hds0 i) v)))) x0 H7 (H9 (bge_le d (trans
hds0 i) H5))))))) H6)))) x_x)))))) H2))))))))))))))) hds).
+(* COMMENTS
+Initial nodes: 1674
+END *)