(* This file was automatically generated: do not edit *********************)
+include "LambdaDelta-1/csubt/pc3.ma".
-
-include "csubt/pc3.ma".
-
-include "csubt/props.ma".
+include "LambdaDelta-1/csubt/props.ma".
theorem csubt_ty3:
\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1
c2) \to (ty3 g c2 u t))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3:
T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t0 t3)).(\lambda (H3: ((\forall
(c2: C).((csubt g (CHead c (Bind b) u) c2) \to (ty3 g c2 t0 t3))))).(\lambda
-(t4: T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t3 t4)).(\lambda (H5:
-((\forall (c2: C).((csubt g (CHead c (Bind b) u) c2) \to (ty3 g c2 t3
-t4))))).(\lambda (c2: C).(\lambda (H6: (csubt g c c2)).(ty3_bind g c2 u t (H1
-c2 H6) b t0 t3 (H3 (CHead c2 (Bind b) u) (csubt_head g c c2 H6 (Bind b) u))
-t4 (H5 (CHead c2 (Bind b) u) (csubt_head g c c2 H6 (Bind b)
-u)))))))))))))))))) (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda
-(_: (ty3 g c w u)).(\lambda (H1: ((\forall (c2: C).((csubt g c c2) \to (ty3 g
-c2 w u))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead
-(Bind Abst) u t))).(\lambda (H3: ((\forall (c2: C).((csubt g c c2) \to (ty3 g
-c2 v (THead (Bind Abst) u t)))))).(\lambda (c2: C).(\lambda (H4: (csubt g c
+(c2: C).(\lambda (H4: (csubt g c c2)).(ty3_bind g c2 u t (H1 c2 H4) b t0 t3
+(H3 (CHead c2 (Bind b) u) (csubt_head g c c2 H4 (Bind b) u)))))))))))))))
+(\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c w
+u)).(\lambda (H1: ((\forall (c2: C).((csubt g c c2) \to (ty3 g c2 w
+u))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead (Bind
+Abst) u t))).(\lambda (H3: ((\forall (c2: C).((csubt g c c2) \to (ty3 g c2 v
+(THead (Bind Abst) u t)))))).(\lambda (c2: C).(\lambda (H4: (csubt g c
c2)).(ty3_appl g c2 w u (H1 c2 H4) v t (H3 c2 H4))))))))))))) (\lambda (c:
C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 g c t0 t3)).(\lambda
(H1: ((\forall (c2: C).((csubt g c c2) \to (ty3 g c2 t0 t3))))).(\lambda (t4: