(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/pc3/dec.ma".
+include "Basic-1/pc3/dec.ma".
-include "LambdaDelta-1/getl/flt.ma".
+include "Basic-1/getl/flt.ma".
-include "LambdaDelta-1/getl/dec.ma".
+include "Basic-1/getl/dec.ma".
theorem ty3_inference:
\forall (g: G).(\forall (c: C).(\forall (t1: T).(or (ex T (\lambda (t2:
T).(ty3 g c2 x0 t4)) False (\lambda (x: T).(\lambda (_: (ty3 g c2 x0 x)).(H5
x0 H9))) (ty3_correct g c2 t x0 H9)))))) (ty3_gen_cast g c2 t0 t t3 H6))))))
H4))) f H2))) k H1))))))) t2))) c t1))).
+(* COMMENTS
+Initial nodes: 9001
+END *)