(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props".
-
-include "ty3/pr3.ma".
+include "LambdaDelta-1/ty3/pr3.ma".
theorem ty3_cred_pr2:
\forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (v2: T).((pr2 c v1
\def H_x in (or_ind (land (lt n x1) (eq T x0 (TLRef n))) (land (le (plus x1
h) n) (eq T x0 (TLRef (minus n h)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h
x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H7:
-(land (lt n x1) (eq T x0 (TLRef n)))).(and_ind (lt n x1) (eq T x0 (TLRef n))
+(land (lt n x1) (eq T x0 (TLRef n)))).(land_ind (lt n x1) (eq T x0 (TLRef n))
(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda
(t2: T).(ty3 g e x0 t2))) (\lambda (H8: (lt n x1)).(\lambda (H9: (eq T x0
(TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ex2 T (\lambda (t2:
n e x3 x2 H12 x4 H18)) x1 (le_plus_minus (S n) x1 H8))))) H16)))))))))
(getl_drop_conf_lt Abbr c0 d0 u n H1 e h (minus x1 (S n)) H10))) x0 H9)))
H7)) (\lambda (H7: (land (le (plus x1 h) n) (eq T x0 (TLRef (minus n
-h))))).(and_ind (le (plus x1 h) n) (eq T x0 (TLRef (minus n h))) (ex2 T
+h))))).(land_ind (le (plus x1 h) n) (eq T x0 (TLRef (minus n h))) (ex2 T
(\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2:
T).(ty3 g e x0 t2))) (\lambda (H8: (le (plus x1 h) n)).(\lambda (H9: (eq T x0
(TLRef (minus n h)))).(eq_ind_r T (TLRef (minus n h)) (\lambda (t0: T).(ex2 T
\def H_x in (or_ind (land (lt n x1) (eq T x0 (TLRef n))) (land (le (plus x1
h) n) (eq T x0 (TLRef (minus n h)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h
x1 t2) (lift (S n) O u))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H7:
-(land (lt n x1) (eq T x0 (TLRef n)))).(and_ind (lt n x1) (eq T x0 (TLRef n))
+(land (lt n x1) (eq T x0 (TLRef n)))).(land_ind (lt n x1) (eq T x0 (TLRef n))
(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) (\lambda
(t2: T).(ty3 g e x0 t2))) (\lambda (H8: (lt n x1)).(\lambda (H9: (eq T x0
(TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ex2 T (\lambda (t2:
(le_O_n (minus x1 (S n))))) (ty3_abst g n e x3 x2 H12 x4 H18)) x1
(le_plus_minus (S n) x1 H8))))) H16)) u H11)))))))) (getl_drop_conf_lt Abst
c0 d0 u n H1 e h (minus x1 (S n)) H10))) x0 H9))) H7)) (\lambda (H7: (land
-(le (plus x1 h) n) (eq T x0 (TLRef (minus n h))))).(and_ind (le (plus x1 h)
+(le (plus x1 h) n) (eq T x0 (TLRef (minus n h))))).(land_ind (le (plus x1 h)
n) (eq T x0 (TLRef (minus n h))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1
t2) (lift (S n) O u))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H8: (le
(plus x1 h) n)).(\lambda (H9: (eq T x0 (TLRef (minus n h)))).(eq_ind_r T