(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/sty0/defs.ma".
+include "Basic-1/sty0/defs.ma".
-include "LambdaDelta-1/getl/drop.ma".
+include "Basic-1/getl/drop.ma".
theorem sty0_lift:
\forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((sty0 g e
(s (Flat Cast) d) H4)) (lift h d (THead (Flat Cast) v2 t4)) (lift_head (Flat
Cast) v2 t4 h d)) (lift h d (THead (Flat Cast) v1 t3)) (lift_head (Flat Cast)
v1 t3 h d))))))))))))))) e t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 3677
+END *)
theorem sty0_correct:
\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty0 g c
(sty0 g c0 t3 x0)).(ex_intro T (\lambda (t4: T).(sty0 g c0 (THead (Flat Cast)
v2 t3) t4)) (THead (Flat Cast) x x0) (sty0_cast g c0 v2 x H5 t3 x0 H7))))
H6)))) H4))))))))))) c t1 t H))))).
+(* COMMENTS
+Initial nodes: 991
+END *)