include "LambdaDelta-1/leq/asucc.ma".
-include "LambdaDelta-1/leq/fwd.ma".
-
include "LambdaDelta-1/getl/drop.ma".
theorem arity_gen_sort:
Cast) u t)) \to (land (arity g c0 u (asucc g a1)) (arity g c0 t a1)))) H2
(THead (Flat Cast) u t) H5) in (let H7 \def (eq_ind T t0 (\lambda (t1:
T).(arity g c0 t1 a1)) H1 (THead (Flat Cast) u t) H5) in (let H8 \def (H6
-(refl_equal T (THead (Flat Cast) u t))) in (and_ind (arity g c0 u (asucc g
+(refl_equal T (THead (Flat Cast) u t))) in (land_ind (arity g c0 u (asucc g
a1)) (arity g c0 t a1) (land (arity g c0 u (asucc g a2)) (arity g c0 t a2))
(\lambda (H9: (arity g c0 u (asucc g a1))).(\lambda (H10: (arity g c0 t
a1)).(conj (arity g c0 u (asucc g a2)) (arity g c0 t a2) (arity_repl g c0 u
(lift_gen_lref x0 x h i H4) in (let H6 \def H_x in (or_ind (land (lt i x) (eq
T x0 (TLRef i))) (land (le (plus x h) i) (eq T x0 (TLRef (minus i h))))
(arity g c2 x0 a0) (\lambda (H7: (land (lt i x) (eq T x0 (TLRef
-i)))).(and_ind (lt i x) (eq T x0 (TLRef i)) (arity g c2 x0 a0) (\lambda (H8:
+i)))).(land_ind (lt i x) (eq T x0 (TLRef i)) (arity g c2 x0 a0) (\lambda (H8:
(lt i x)).(\lambda (H9: (eq T x0 (TLRef i))).(eq_ind_r T (TLRef i) (\lambda
(t0: T).(arity g c2 t0 a0)) (let H10 \def (eq_ind nat x (\lambda (n:
nat).(drop h n c c2)) H5 (S (plus i (minus x (S i)))) (lt_plus_minus i x H8))
(arity_abbr g c2 x2 x1 i H12 a0 (H14 (minus x (S i)) x1 (refl_equal T (lift h
(minus x (S i)) x1)) x2 H13))))))))) (getl_drop_conf_lt Abbr c d0 u i H1 c2 h
(minus x (S i)) H10))) x0 H9))) H7)) (\lambda (H7: (land (le (plus x h) i)
-(eq T x0 (TLRef (minus i h))))).(and_ind (le (plus x h) i) (eq T x0 (TLRef
+(eq T x0 (TLRef (minus i h))))).(land_ind (le (plus x h) i) (eq T x0 (TLRef
(minus i h))) (arity g c2 x0 a0) (\lambda (H8: (le (plus x h) i)).(\lambda
(H9: (eq T x0 (TLRef (minus i h)))).(eq_ind_r T (TLRef (minus i h)) (\lambda
(t0: T).(arity g c2 t0 a0)) (arity_abbr g c2 d0 u (minus i h)
(lift_gen_lref x0 x h i H4) in (let H6 \def H_x in (or_ind (land (lt i x) (eq
T x0 (TLRef i))) (land (le (plus x h) i) (eq T x0 (TLRef (minus i h))))
(arity g c2 x0 a0) (\lambda (H7: (land (lt i x) (eq T x0 (TLRef
-i)))).(and_ind (lt i x) (eq T x0 (TLRef i)) (arity g c2 x0 a0) (\lambda (H8:
+i)))).(land_ind (lt i x) (eq T x0 (TLRef i)) (arity g c2 x0 a0) (\lambda (H8:
(lt i x)).(\lambda (H9: (eq T x0 (TLRef i))).(eq_ind_r T (TLRef i) (\lambda
(t0: T).(arity g c2 t0 a0)) (let H10 \def (eq_ind nat x (\lambda (n:
nat).(drop h n c c2)) H5 (S (plus i (minus x (S i)))) (lt_plus_minus i x H8))
x (S i)) x1) H11) in (arity_abst g c2 x2 x1 i H12 a0 (H14 (minus x (S i)) x1
(refl_equal T (lift h (minus x (S i)) x1)) x2 H13))))))))) (getl_drop_conf_lt
Abst c d0 u i H1 c2 h (minus x (S i)) H10))) x0 H9))) H7)) (\lambda (H7:
-(land (le (plus x h) i) (eq T x0 (TLRef (minus i h))))).(and_ind (le (plus x
+(land (le (plus x h) i) (eq T x0 (TLRef (minus i h))))).(land_ind (le (plus x
h) i) (eq T x0 (TLRef (minus i h))) (arity g c2 x0 a0) (\lambda (H8: (le
(plus x h) i)).(\lambda (H9: (eq T x0 (TLRef (minus i h)))).(eq_ind_r T
(TLRef (minus i h)) (\lambda (t0: T).(arity g c2 t0 a0)) (arity_abst g c2 d0