(* This file was automatically generated: do not edit *********************)
-include "Basic-1/sty1/props.ma".
+include "basic_1/sty1/props.ma".
-include "Basic-1/cnt/props.ma".
+include "basic_1/cnt/props.ma".
-theorem sty1_cnt:
+lemma sty1_cnt:
\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty0 g c
t1 t) \to (ex2 T (\lambda (t2: T).(sty1 g c t1 t2)) (\lambda (t2: T).(cnt
t2)))))))
x))).(ex_intro2 T (\lambda (t4: T).(sty1 g c0 (THead (Flat Cast) v1 t2) t4))
(\lambda (t4: T).(cnt t4)) (THead (Flat Cast) x0 x) H9 (cnt_head x H6 (Flat
Cast) x0))))) H7)))))) H4))))))))))) c t1 t H))))).
-(* COMMENTS
-Initial nodes: 1313
-END *)