(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1".
+include "LambdaDelta-1/ty3/props.ma".
-include "ty3/props.ma".
+include "LambdaDelta-1/pc3/subst1.ma".
-include "pc3/subst1.ma".
-
-include "pc3/fwd.ma".
-
-include "csubst1/getl.ma".
-
-include "csubst1/fwd.ma".
-
-include "getl/getl.ma".
+include "LambdaDelta-1/getl/getl.ma".
theorem ty3_gen_cabbr:
\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c
O)) a d u (getl_drop_conf_ge n (CHead d (Bind Abbr) u) a0 (csubst1_getl_ge d0
n (le_S_n d0 n (le_S (S d0) n H6)) c0 a0 u0 H4 (CHead d (Bind Abbr) u) H0) a
(S O) d0 H5 (eq_ind_r nat (plus (S O) d0) (\lambda (n0: nat).(le n0 n)) H6
-(plus d0 (S O)) (plus_comm d0 (S O)))) t H1) n (minus_x_SO n (le_lt_trans O
-d0 n (le_O_n d0) H6)))) (plus (S O) (minus n (S O))) (plus_comm (S O) (minus
-n (S O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus O (minus n
-(S O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0)
+(plus d0 (S O)) (plus_sym d0 (S O)))) t H1) n (minus_x_SO n (le_lt_trans O d0
+n (le_O_n d0) H6)))) (plus (S O) (minus n (S O))) (plus_sym (S O) (minus n (S
+O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus O (minus n (S
+O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0)
H6))))))))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d:
C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abst)
u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (e:
O)) a d u (getl_drop_conf_ge n (CHead d (Bind Abst) u) a0 (csubst1_getl_ge d0
n (le_S_n d0 n (le_S (S d0) n H6)) c0 a0 u0 H4 (CHead d (Bind Abst) u) H0) a
(S O) d0 H5 (eq_ind_r nat (plus (S O) d0) (\lambda (n0: nat).(le n0 n)) H6
-(plus d0 (S O)) (plus_comm d0 (S O)))) t H1) n (minus_x_SO n (le_lt_trans O
-d0 n (le_O_n d0) H6)))) (plus (S O) (minus n (S O))) (plus_comm (S O) (minus
-n (S O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus O (minus n
-(S O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0)
+(plus d0 (S O)) (plus_sym d0 (S O)))) t H1) n (minus_x_SO n (le_lt_trans O d0
+n (le_O_n d0) H6)))) (plus (S O) (minus n (S O))) (plus_sym (S O) (minus n (S
+O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus O (minus n (S
+O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0)
H6))))))))))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (t:
T).(\lambda (_: (ty3 g c0 u t)).(\lambda (H1: ((\forall (e: C).(\forall (u0:
T).(\forall (d: nat).((getl d c0 (CHead e (Bind Abbr) u0)) \to (\forall (a0:
O))) (\lambda (n0: nat).(ty3 g a (TLRef (minus n (S O))) (lift n0 O t)))
(ty3_abbr g (minus n (S O)) a d u (getl_drop_conf_ge n (CHead d (Bind Abbr)
u) c0 H0 a (S O) d0 H4 (eq_ind_r nat (plus (S O) d0) (\lambda (n0: nat).(le
-n0 n)) H5 (plus d0 (S O)) (plus_comm d0 (S O)))) t H1) n (minus_x_SO n
-(le_lt_trans O d0 n (le_O_n d0) H5)))) (plus (S O) (minus n (S O)))
-(plus_comm (S O) (minus n (S O)))) (S (plus O (minus n (S O)))) (refl_equal
-nat (S (plus O (minus n (S O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n
-(le_O_n d0) H5))))))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda
-(d: C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abst)
+n0 n)) H5 (plus d0 (S O)) (plus_sym d0 (S O)))) t H1) n (minus_x_SO n
+(le_lt_trans O d0 n (le_O_n d0) H5)))) (plus (S O) (minus n (S O))) (plus_sym
+(S O) (minus n (S O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus
+O (minus n (S O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0)
+H5))))))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d:
+C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abst)
u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (e:
C).(\forall (u0: T).(\forall (d0: nat).((getl d0 d (CHead e (Bind Void) u0))
\to (\forall (a: C).((drop (S O) d0 d a) \to (ex3_2 T T (\lambda (y1:
(eq_ind_r nat (S (minus n (S O))) (\lambda (n0: nat).(ty3 g a (TLRef (minus n
(S O))) (lift n0 O u))) (ty3_abst g (minus n (S O)) a d u (getl_drop_conf_ge
n (CHead d (Bind Abst) u) c0 H0 a (S O) d0 H4 (eq_ind_r nat (plus (S O) d0)
-(\lambda (n0: nat).(le n0 n)) H5 (plus d0 (S O)) (plus_comm d0 (S O)))) t H1)
+(\lambda (n0: nat).(le n0 n)) H5 (plus d0 (S O)) (plus_sym d0 (S O)))) t H1)
n (minus_x_SO n (le_lt_trans O d0 n (le_O_n d0) H5)))) (plus (S O) (minus n
-(S O))) (plus_comm (S O) (minus n (S O)))) (S (plus O (minus n (S O))))
+(S O))) (plus_sym (S O) (minus n (S O)))) (S (plus O (minus n (S O))))
(refl_equal nat (S (plus O (minus n (S O)))))) n (lt_plus_minus O n
(le_lt_trans O d0 n (le_O_n d0) H5))))))))))))))))))) (\lambda (c0:
C).(\lambda (u: T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 u t)).(\lambda