X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcsuba%2Farity.ma;h=7b35a4381bb36b2440172e20b3e2a68ca3c96b78;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=3307ed325525590e7a8bb618721f524f97d3f635;hpb=f7b122ac0979ee71c222d09d3ce32ded37767cd5;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/csuba/arity.ma b/matita/matita/contribs/lambdadelta/basic_1/csuba/arity.ma
index 3307ed325..7b35a4381 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csuba/arity.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csuba/arity.ma
@@ -22,403 +22,264 @@ include "basic_1/arity/fwd.ma".
 
 include "basic_1/csubv/getl.ma".
 
-theorem csuba_arity:
+lemma csuba_arity:
  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1 
 t a) \to (\forall (c2: C).((csuba g c1 c2) \to (arity g c2 t a)))))))
 \def
  \lambda (g: G).(\lambda (c1: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H: 
-(arity g c1 t a)).(let TMP_1 \def (\lambda (c: C).(\lambda (t0: T).(\lambda 
-(a0: A).(\forall (c2: C).((csuba g c c2) \to (arity g c2 t0 a0)))))) in (let 
-TMP_2 \def (\lambda (c: C).(\lambda (n: nat).(\lambda (c2: C).(\lambda (_: 
-(csuba g c c2)).(arity_sort g c2 n))))) in (let TMP_11 \def (\lambda (c: 
+(arity g c1 t a)).(arity_ind g (\lambda (c: C).(\lambda (t0: T).(\lambda (a0: 
+A).(\forall (c2: C).((csuba g c c2) \to (arity g c2 t0 a0)))))) (\lambda (c: 
+C).(\lambda (n: nat).(\lambda (c2: C).(\lambda (_: (csuba g c 
+c2)).(arity_sort g c2 n))))) (\lambda (c: C).(\lambda (d: C).(\lambda (u: 
+T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abbr) 
+u))).(\lambda (a0: A).(\lambda (_: (arity g d u a0)).(\lambda (H2: ((\forall 
+(c2: C).((csuba g d c2) \to (arity g c2 u a0))))).(\lambda (c2: C).(\lambda 
+(H3: (csuba g c c2)).(let H4 \def (csuba_getl_abbr g c d u i H0 c2 H3) in 
+(ex2_ind C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u))) (\lambda 
+(d2: C).(csuba g d d2)) (arity g c2 (TLRef i) a0) (\lambda (x: C).(\lambda 
+(H5: (getl i c2 (CHead x (Bind Abbr) u))).(\lambda (H6: (csuba g d 
+x)).(arity_abbr g c2 x u i H5 a0 (H2 x H6))))) H4)))))))))))) (\lambda (c: 
 C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c 
-(CHead d (Bind Abbr) u))).(\lambda (a0: A).(\lambda (_: (arity g d u 
-a0)).(\lambda (H2: ((\forall (c2: C).((csuba g d c2) \to (arity g c2 u 
-a0))))).(\lambda (c2: C).(\lambda (H3: (csuba g c c2)).(let H4 \def 
-(csuba_getl_abbr g c d u i H0 c2 H3) in (let TMP_5 \def (\lambda (d2: C).(let 
-TMP_3 \def (Bind Abbr) in (let TMP_4 \def (CHead d2 TMP_3 u) in (getl i c2 
-TMP_4)))) in (let TMP_6 \def (\lambda (d2: C).(csuba g d d2)) in (let TMP_7 
-\def (TLRef i) in (let TMP_8 \def (arity g c2 TMP_7 a0) in (let TMP_10 \def 
-(\lambda (x: C).(\lambda (H5: (getl i c2 (CHead x (Bind Abbr) u))).(\lambda 
-(H6: (csuba g d x)).(let TMP_9 \def (H2 x H6) in (arity_abbr g c2 x u i H5 a0 
-TMP_9))))) in (ex2_ind C TMP_5 TMP_6 TMP_8 TMP_10 H4))))))))))))))))) in (let 
-TMP_53 \def (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: 
-nat).(\lambda (H0: (getl i c (CHead d (Bind Abst) u))).(\lambda (a0: 
-A).(\lambda (H1: (arity g d u (asucc g a0))).(\lambda (H2: ((\forall (c2: 
-C).((csuba g d c2) \to (arity g c2 u (asucc g a0)))))).(\lambda (c2: 
-C).(\lambda (H3: (csuba g c c2)).(let H4 \def (csuba_getl_abst g c d u i H0 
-c2 H3) in (let TMP_14 \def (\lambda (d2: C).(let TMP_12 \def (Bind Abst) in 
-(let TMP_13 \def (CHead d2 TMP_12 u) in (getl i c2 TMP_13)))) in (let TMP_15 
-\def (\lambda (d2: C).(csuba g d d2)) in (let TMP_16 \def (ex2 C TMP_14 
-TMP_15) in (let TMP_19 \def (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: 
-A).(let TMP_17 \def (Bind Abbr) in (let TMP_18 \def (CHead d2 TMP_17 u2) in 
-(getl i c2 TMP_18)))))) in (let TMP_20 \def (\lambda (d2: C).(\lambda (_: 
-T).(\lambda (_: A).(csuba g d d2)))) in (let TMP_22 \def (\lambda (_: 
-C).(\lambda (_: T).(\lambda (a1: A).(let TMP_21 \def (asucc g a1) in (arity g 
-d u TMP_21))))) in (let TMP_23 \def (\lambda (d2: C).(\lambda (u2: 
-T).(\lambda (a1: A).(arity g d2 u2 a1)))) in (let TMP_24 \def (ex4_3 C T A 
-TMP_19 TMP_20 TMP_22 TMP_23) in (let TMP_25 \def (TLRef i) in (let TMP_26 
-\def (arity g c2 TMP_25 a0) in (let TMP_35 \def (\lambda (H5: (ex2 C (\lambda 
-(d2: C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d 
-d2)))).(let TMP_29 \def (\lambda (d2: C).(let TMP_27 \def (Bind Abst) in (let 
-TMP_28 \def (CHead d2 TMP_27 u) in (getl i c2 TMP_28)))) in (let TMP_30 \def 
-(\lambda (d2: C).(csuba g d d2)) in (let TMP_31 \def (TLRef i) in (let TMP_32 
-\def (arity g c2 TMP_31 a0) in (let TMP_34 \def (\lambda (x: C).(\lambda (H6: 
-(getl i c2 (CHead x (Bind Abst) u))).(\lambda (H7: (csuba g d x)).(let TMP_33 
-\def (H2 x H7) in (arity_abst g c2 x u i H6 a0 TMP_33))))) in (ex2_ind C 
-TMP_29 TMP_30 TMP_32 TMP_34 H5))))))) in (let TMP_52 \def (\lambda (H5: 
-(ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 
-(CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: 
-A).(csuba g d d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a1: A).(arity 
-g d u (asucc g a1))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a1: 
-A).(arity g d2 u2 a1)))))).(let TMP_38 \def (\lambda (d2: C).(\lambda (u2: 
-T).(\lambda (_: A).(let TMP_36 \def (Bind Abbr) in (let TMP_37 \def (CHead d2 
-TMP_36 u2) in (getl i c2 TMP_37)))))) in (let TMP_39 \def (\lambda (d2: 
-C).(\lambda (_: T).(\lambda (_: A).(csuba g d d2)))) in (let TMP_41 \def 
-(\lambda (_: C).(\lambda (_: T).(\lambda (a1: A).(let TMP_40 \def (asucc g 
-a1) in (arity g d u TMP_40))))) in (let TMP_42 \def (\lambda (d2: C).(\lambda 
-(u2: T).(\lambda (a1: A).(arity g d2 u2 a1)))) in (let TMP_43 \def (TLRef i) 
-in (let TMP_44 \def (arity g c2 TMP_43 a0) in (let TMP_51 \def (\lambda (x0: 
-C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H6: (getl i c2 (CHead x0 (Bind 
-Abbr) x1))).(\lambda (_: (csuba g d x0)).(\lambda (H8: (arity g d u (asucc g 
-x2))).(\lambda (H9: (arity g x0 x1 x2)).(let TMP_45 \def (TLRef i) in (let 
-TMP_46 \def (arity_abbr g c2 x0 x1 i H6 x2 H9) in (let TMP_47 \def (asucc g 
-x2) in (let TMP_48 \def (asucc g a0) in (let TMP_49 \def (arity_mono g d u 
-TMP_47 H8 TMP_48 H1) in (let TMP_50 \def (asucc_inj g x2 a0 TMP_49) in 
-(arity_repl g c2 TMP_45 x2 TMP_46 a0 TMP_50)))))))))))))) in (ex4_3_ind C T A 
-TMP_38 TMP_39 TMP_41 TMP_42 TMP_44 TMP_51 H5))))))))) in (or_ind TMP_16 
-TMP_24 TMP_26 TMP_35 TMP_52 H4)))))))))))))))))))))))) in (let TMP_60 \def 
-(\lambda (b: B).(\lambda (H0: (not (eq B b Abst))).(\lambda (c: C).(\lambda 
-(u: T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H2: 
+(CHead d (Bind Abst) u))).(\lambda (a0: A).(\lambda (H1: (arity g d u (asucc 
+g a0))).(\lambda (H2: ((\forall (c2: C).((csuba g d c2) \to (arity g c2 u 
+(asucc g a0)))))).(\lambda (c2: C).(\lambda (H3: (csuba g c c2)).(let H4 \def 
+(csuba_getl_abst g c d u i H0 c2 H3) in (or_ind (ex2 C (\lambda (d2: C).(getl 
+i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d d2))) (ex4_3 C T 
+A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 
+(Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g 
+d d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a1: A).(arity g d u (asucc 
+g a1))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a1: A).(arity g d2 u2 
+a1))))) (arity g c2 (TLRef i) a0) (\lambda (H5: (ex2 C (\lambda (d2: C).(getl 
+i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d d2)))).(ex2_ind C 
+(\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: 
+C).(csuba g d d2)) (arity g c2 (TLRef i) a0) (\lambda (x: C).(\lambda (H6: 
+(getl i c2 (CHead x (Bind Abst) u))).(\lambda (H7: (csuba g d x)).(arity_abst 
+g c2 x u i H6 a0 (H2 x H7))))) H5)) (\lambda (H5: (ex4_3 C T A (\lambda (d2: 
+C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abbr) u2))))) 
+(\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d d2)))) (\lambda 
+(_: C).(\lambda (_: T).(\lambda (a1: A).(arity g d u (asucc g a1))))) 
+(\lambda (d2: C).(\lambda (u2: T).(\lambda (a1: A).(arity g d2 u2 
+a1)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: 
+A).(getl i c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: 
+T).(\lambda (_: A).(csuba g d d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda 
+(a1: A).(arity g d u (asucc g a1))))) (\lambda (d2: C).(\lambda (u2: 
+T).(\lambda (a1: A).(arity g d2 u2 a1)))) (arity g c2 (TLRef i) a0) (\lambda 
+(x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H6: (getl i c2 (CHead x0 
+(Bind Abbr) x1))).(\lambda (_: (csuba g d x0)).(\lambda (H8: (arity g d u 
+(asucc g x2))).(\lambda (H9: (arity g x0 x1 x2)).(arity_repl g c2 (TLRef i) 
+x2 (arity_abbr g c2 x0 x1 i H6 x2 H9) a0 (asucc_inj g x2 a0 (arity_mono g d u 
+(asucc g x2) H8 (asucc g a0) H1)))))))))) H5)) H4)))))))))))) (\lambda (b: 
+B).(\lambda (H0: (not (eq B b Abst))).(\lambda (c: C).(\lambda (u: 
+T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H2: ((\forall 
+(c2: C).((csuba g c c2) \to (arity g c2 u a1))))).(\lambda (t0: T).(\lambda 
+(a2: A).(\lambda (_: (arity g (CHead c (Bind b) u) t0 a2)).(\lambda (H4: 
+((\forall (c2: C).((csuba g (CHead c (Bind b) u) c2) \to (arity g c2 t0 
+a2))))).(\lambda (c2: C).(\lambda (H5: (csuba g c c2)).(arity_bind g b H0 c2 
+u a1 (H2 c2 H5) t0 a2 (H4 (CHead c2 (Bind b) u) (csuba_head g c c2 H5 (Bind 
+b) u)))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a1: 
+A).(\lambda (_: (arity g c u (asucc g a1))).(\lambda (H1: ((\forall (c2: 
+C).((csuba g c c2) \to (arity g c2 u (asucc g a1)))))).(\lambda (t0: 
+T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c (Bind Abst) u) t0 
+a2)).(\lambda (H3: ((\forall (c2: C).((csuba g (CHead c (Bind Abst) u) c2) 
+\to (arity g c2 t0 a2))))).(\lambda (c2: C).(\lambda (H4: (csuba g c 
+c2)).(arity_head g c2 u a1 (H1 c2 H4) t0 a2 (H3 (CHead c2 (Bind Abst) u) 
+(csuba_head g c c2 H4 (Bind Abst) u)))))))))))))) (\lambda (c: C).(\lambda 
+(u: T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H1: 
 ((\forall (c2: C).((csuba g c c2) \to (arity g c2 u a1))))).(\lambda (t0: 
-T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c (Bind b) u) t0 
-a2)).(\lambda (H4: ((\forall (c2: C).((csuba g (CHead c (Bind b) u) c2) \to 
-(arity g c2 t0 a2))))).(\lambda (c2: C).(\lambda (H5: (csuba g c c2)).(let 
-TMP_54 \def (H2 c2 H5) in (let TMP_55 \def (Bind b) in (let TMP_56 \def 
-(CHead c2 TMP_55 u) in (let TMP_57 \def (Bind b) in (let TMP_58 \def 
-(csuba_head g c c2 H5 TMP_57 u) in (let TMP_59 \def (H4 TMP_56 TMP_58) in 
-(arity_bind g b H0 c2 u a1 TMP_54 t0 a2 TMP_59)))))))))))))))))))) in (let 
-TMP_67 \def (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: 
-(arity g c u (asucc g a1))).(\lambda (H1: ((\forall (c2: C).((csuba g c c2) 
-\to (arity g c2 u (asucc g a1)))))).(\lambda (t0: T).(\lambda (a2: 
-A).(\lambda (_: (arity g (CHead c (Bind Abst) u) t0 a2)).(\lambda (H3: 
-((\forall (c2: C).((csuba g (CHead c (Bind Abst) u) c2) \to (arity g c2 t0 
-a2))))).(\lambda (c2: C).(\lambda (H4: (csuba g c c2)).(let TMP_61 \def (H1 
-c2 H4) in (let TMP_62 \def (Bind Abst) in (let TMP_63 \def (CHead c2 TMP_62 
-u) in (let TMP_64 \def (Bind Abst) in (let TMP_65 \def (csuba_head g c c2 H4 
-TMP_64 u) in (let TMP_66 \def (H3 TMP_63 TMP_65) in (arity_head g c2 u a1 
-TMP_61 t0 a2 TMP_66)))))))))))))))))) in (let TMP_70 \def (\lambda (c: 
-C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda 
-(H1: ((\forall (c2: C).((csuba g c c2) \to (arity g c2 u a1))))).(\lambda 
-(t0: T).(\lambda (a2: A).(\lambda (_: (arity g c t0 (AHead a1 a2))).(\lambda 
-(H3: ((\forall (c2: C).((csuba g c c2) \to (arity g c2 t0 (AHead a1 
-a2)))))).(\lambda (c2: C).(\lambda (H4: (csuba g c c2)).(let TMP_68 \def (H1 
-c2 H4) in (let TMP_69 \def (H3 c2 H4) in (arity_appl g c2 u a1 TMP_68 t0 a2 
-TMP_69)))))))))))))) in (let TMP_73 \def (\lambda (c: C).(\lambda (u: 
+T).(\lambda (a2: A).(\lambda (_: (arity g c t0 (AHead a1 a2))).(\lambda (H3: 
+((\forall (c2: C).((csuba g c c2) \to (arity g c2 t0 (AHead a1 
+a2)))))).(\lambda (c2: C).(\lambda (H4: (csuba g c c2)).(arity_appl g c2 u a1 
+(H1 c2 H4) t0 a2 (H3 c2 H4))))))))))))) (\lambda (c: C).(\lambda (u: 
 T).(\lambda (a0: A).(\lambda (_: (arity g c u (asucc g a0))).(\lambda (H1: 
 ((\forall (c2: C).((csuba g c c2) \to (arity g c2 u (asucc g 
 a0)))))).(\lambda (t0: T).(\lambda (_: (arity g c t0 a0)).(\lambda (H3: 
 ((\forall (c2: C).((csuba g c c2) \to (arity g c2 t0 a0))))).(\lambda (c2: 
-C).(\lambda (H4: (csuba g c c2)).(let TMP_71 \def (H1 c2 H4) in (let TMP_72 
-\def (H3 c2 H4) in (arity_cast g c2 u a0 TMP_71 t0 TMP_72))))))))))))) in 
-(let TMP_75 \def (\lambda (c: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda 
-(_: (arity g c t0 a1)).(\lambda (H1: ((\forall (c2: C).((csuba g c c2) \to 
-(arity g c2 t0 a1))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda 
-(c2: C).(\lambda (H3: (csuba g c c2)).(let TMP_74 \def (H1 c2 H3) in 
-(arity_repl g c2 t0 a1 TMP_74 a2 H2))))))))))) in (arity_ind g TMP_1 TMP_2 
-TMP_11 TMP_53 TMP_60 TMP_67 TMP_70 TMP_73 TMP_75 c1 t a H)))))))))))))).
+C).(\lambda (H4: (csuba g c c2)).(arity_cast g c2 u a0 (H1 c2 H4) t0 (H3 c2 
+H4)))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda (_: 
+(arity g c t0 a1)).(\lambda (H1: ((\forall (c2: C).((csuba g c c2) \to (arity 
+g c2 t0 a1))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2: 
+C).(\lambda (H3: (csuba g c c2)).(arity_repl g c2 t0 a1 (H1 c2 H3) a2 
+H2)))))))))) c1 t a H))))).
 
-theorem csuba_arity_rev:
+lemma csuba_arity_rev:
  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1 
 t a) \to (\forall (c2: C).((csuba g c2 c1) \to ((csubv c2 c1) \to (arity g c2 
 t a))))))))
 \def
  \lambda (g: G).(\lambda (c1: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H: 
-(arity g c1 t a)).(let TMP_1 \def (\lambda (c: C).(\lambda (t0: T).(\lambda 
-(a0: A).(\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 t0 
-a0))))))) in (let TMP_2 \def (\lambda (c: C).(\lambda (n: nat).(\lambda (c2: 
-C).(\lambda (_: (csuba g c2 c)).(\lambda (_: (csubv c2 c)).(arity_sort g c2 
-n)))))) in (let TMP_142 \def (\lambda (c: C).(\lambda (d: C).(\lambda (u: 
-T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abbr) 
-u))).(\lambda (a0: A).(\lambda (H1: (arity g d u a0)).(\lambda (H2: ((\forall 
-(c2: C).((csuba g c2 d) \to ((csubv c2 d) \to (arity g c2 u a0)))))).(\lambda 
-(c2: C).(\lambda (H3: (csuba g c2 c)).(\lambda (H4: (csubv c2 c)).(let H_x 
-\def (csuba_getl_abbr_rev g c d u i H0 c2 H3) in (let H5 \def H_x in (let 
-TMP_5 \def (\lambda (d2: C).(let TMP_3 \def (Bind Abbr) in (let TMP_4 \def 
-(CHead d2 TMP_3 u) in (getl i c2 TMP_4)))) in (let TMP_6 \def (\lambda (d2: 
-C).(csuba g d2 d)) in (let TMP_7 \def (ex2 C TMP_5 TMP_6) in (let TMP_10 \def 
-(\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(let TMP_8 \def (Bind Abst) 
-in (let TMP_9 \def (CHead d2 TMP_8 u2) in (getl i c2 TMP_9)))))) in (let 
-TMP_11 \def (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 
-d)))) in (let TMP_13 \def (\lambda (d2: C).(\lambda (u2: T).(\lambda (a1: 
-A).(let TMP_12 \def (asucc g a1) in (arity g d2 u2 TMP_12))))) in (let TMP_14 
-\def (\lambda (_: C).(\lambda (_: T).(\lambda (a1: A).(arity g d u a1)))) in 
-(let TMP_15 \def (ex4_3 C T A TMP_10 TMP_11 TMP_13 TMP_14) in (let TMP_18 
-\def (\lambda (d2: C).(\lambda (u2: T).(let TMP_16 \def (Bind Void) in (let 
-TMP_17 \def (CHead d2 TMP_16 u2) in (getl i c2 TMP_17))))) in (let TMP_19 
-\def (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))) in (let TMP_20 \def 
-(ex2_2 C T TMP_18 TMP_19) in (let TMP_21 \def (TLRef i) in (let TMP_22 \def 
-(arity g c2 TMP_21 a0) in (let TMP_90 \def (\lambda (H6: (ex2 C (\lambda (d2: 
-C).(getl i c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d2 
-d)))).(let TMP_25 \def (\lambda (d2: C).(let TMP_23 \def (Bind Abbr) in (let 
-TMP_24 \def (CHead d2 TMP_23 u) in (getl i c2 TMP_24)))) in (let TMP_26 \def 
-(\lambda (d2: C).(csuba g d2 d)) in (let TMP_27 \def (TLRef i) in (let TMP_28 
-\def (arity g c2 TMP_27 a0) in (let TMP_89 \def (\lambda (x: C).(\lambda (H7: 
-(getl i c2 (CHead x (Bind Abbr) u))).(\lambda (H8: (csuba g x d)).(let H_x0 
-\def (csubv_getl_conf c2 c H4 Abbr x u i H7) in (let H9 \def H_x0 in (let 
-TMP_29 \def (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv x d2)))) 
-in (let TMP_32 \def (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(let 
-TMP_30 \def (Bind b2) in (let TMP_31 \def (CHead d2 TMP_30 v2) in (getl i c 
-TMP_31)))))) in (let TMP_33 \def (TLRef i) in (let TMP_34 \def (arity g c2 
-TMP_33 a0) in (let TMP_88 \def (\lambda (x0: B).(\lambda (x1: C).(\lambda 
-(x2: T).(\lambda (H10: (csubv x x1)).(\lambda (H11: (getl i c (CHead x1 (Bind 
-x0) x2))).(let TMP_35 \def (Bind Abbr) in (let TMP_36 \def (CHead d TMP_35 u) 
-in (let TMP_37 \def (\lambda (c0: C).(getl i c c0)) in (let TMP_38 \def (Bind 
-x0) in (let TMP_39 \def (CHead x1 TMP_38 x2) in (let TMP_40 \def (Bind Abbr) 
-in (let TMP_41 \def (CHead d TMP_40 u) in (let TMP_42 \def (Bind x0) in (let 
-TMP_43 \def (CHead x1 TMP_42 x2) in (let TMP_44 \def (getl_mono c TMP_41 i H0 
-TMP_43 H11) in (let H12 \def (eq_ind C TMP_36 TMP_37 H0 TMP_39 TMP_44) in 
-(let TMP_45 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow d | 
-(CHead c0 _ _) \Rightarrow c0])) in (let TMP_46 \def (Bind Abbr) in (let 
-TMP_47 \def (CHead d TMP_46 u) in (let TMP_48 \def (Bind x0) in (let TMP_49 
-\def (CHead x1 TMP_48 x2) in (let TMP_50 \def (Bind Abbr) in (let TMP_51 \def 
-(CHead d TMP_50 u) in (let TMP_52 \def (Bind x0) in (let TMP_53 \def (CHead 
-x1 TMP_52 x2) in (let TMP_54 \def (getl_mono c TMP_51 i H0 TMP_53 H11) in 
-(let H13 \def (f_equal C C TMP_45 TMP_47 TMP_49 TMP_54) in (let TMP_55 \def 
-(\lambda (e: C).(match e with [(CSort _) \Rightarrow Abbr | (CHead _ k _) 
-\Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow 
-Abbr])])) in (let TMP_56 \def (Bind Abbr) in (let TMP_57 \def (CHead d TMP_56 
-u) in (let TMP_58 \def (Bind x0) in (let TMP_59 \def (CHead x1 TMP_58 x2) in 
-(let TMP_60 \def (Bind Abbr) in (let TMP_61 \def (CHead d TMP_60 u) in (let 
-TMP_62 \def (Bind x0) in (let TMP_63 \def (CHead x1 TMP_62 x2) in (let TMP_64 
-\def (getl_mono c TMP_61 i H0 TMP_63 H11) in (let H14 \def (f_equal C B 
-TMP_55 TMP_57 TMP_59 TMP_64) in (let TMP_65 \def (\lambda (e: C).(match e 
-with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) in (let 
-TMP_66 \def (Bind Abbr) in (let TMP_67 \def (CHead d TMP_66 u) in (let TMP_68 
-\def (Bind x0) in (let TMP_69 \def (CHead x1 TMP_68 x2) in (let TMP_70 \def 
-(Bind Abbr) in (let TMP_71 \def (CHead d TMP_70 u) in (let TMP_72 \def (Bind 
-x0) in (let TMP_73 \def (CHead x1 TMP_72 x2) in (let TMP_74 \def (getl_mono c 
-TMP_71 i H0 TMP_73 H11) in (let H15 \def (f_equal C T TMP_65 TMP_67 TMP_69 
-TMP_74) in (let TMP_86 \def (\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq 
-C d x1)).(let TMP_77 \def (\lambda (t0: T).(let TMP_75 \def (Bind x0) in (let 
-TMP_76 \def (CHead x1 TMP_75 t0) in (getl i c TMP_76)))) in (let H18 \def 
-(eq_ind_r T x2 TMP_77 H12 u H15) in (let TMP_80 \def (\lambda (c0: C).(let 
-TMP_78 \def (Bind x0) in (let TMP_79 \def (CHead c0 TMP_78 u) in (getl i c 
-TMP_79)))) in (let H19 \def (eq_ind_r C x1 TMP_80 H18 d H17) in (let TMP_81 
-\def (\lambda (c0: C).(csubv x c0)) in (let H20 \def (eq_ind_r C x1 TMP_81 
-H10 d H17) in (let TMP_84 \def (\lambda (b: B).(let TMP_82 \def (Bind b) in 
-(let TMP_83 \def (CHead d TMP_82 u) in (getl i c TMP_83)))) in (let H21 \def 
-(eq_ind_r B x0 TMP_84 H19 Abbr H16) in (let TMP_85 \def (H2 x H8 H20) in 
-(arity_abbr g c2 x u i H7 a0 TMP_85)))))))))))) in (let TMP_87 \def (TMP_86 
-H14) in (TMP_87 H13)))))))))))))))))))))))))))))))))))))))))))))))))))) in 
-(ex2_3_ind B C T TMP_29 TMP_32 TMP_34 TMP_88 H9))))))))))) in (ex2_ind C 
-TMP_25 TMP_26 TMP_28 TMP_89 H6))))))) in (let TMP_104 \def (\lambda (H6: 
-(ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 
-(CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: 
-A).(csuba g d2 d)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a1: 
-A).(arity g d2 u2 (asucc g a1))))) (\lambda (_: C).(\lambda (_: T).(\lambda 
-(a1: A).(arity g d u a1)))))).(let TMP_93 \def (\lambda (d2: C).(\lambda (u2: 
-T).(\lambda (_: A).(let TMP_91 \def (Bind Abst) in (let TMP_92 \def (CHead d2 
-TMP_91 u2) in (getl i c2 TMP_92)))))) in (let TMP_94 \def (\lambda (d2: 
-C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d)))) in (let TMP_96 \def 
-(\lambda (d2: C).(\lambda (u2: T).(\lambda (a1: A).(let TMP_95 \def (asucc g 
-a1) in (arity g d2 u2 TMP_95))))) in (let TMP_97 \def (\lambda (_: 
-C).(\lambda (_: T).(\lambda (a1: A).(arity g d u a1)))) in (let TMP_98 \def 
-(TLRef i) in (let TMP_99 \def (arity g c2 TMP_98 a0) in (let TMP_103 \def 
+(arity g c1 t a)).(arity_ind g (\lambda (c: C).(\lambda (t0: T).(\lambda (a0: 
+A).(\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 t0 
+a0))))))) (\lambda (c: C).(\lambda (n: nat).(\lambda (c2: C).(\lambda (_: 
+(csuba g c2 c)).(\lambda (_: (csubv c2 c)).(arity_sort g c2 n)))))) (\lambda 
+(c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl 
+i c (CHead d (Bind Abbr) u))).(\lambda (a0: A).(\lambda (H1: (arity g d u 
+a0)).(\lambda (H2: ((\forall (c2: C).((csuba g c2 d) \to ((csubv c2 d) \to 
+(arity g c2 u a0)))))).(\lambda (c2: C).(\lambda (H3: (csuba g c2 
+c)).(\lambda (H4: (csubv c2 c)).(let H_x \def (csuba_getl_abbr_rev g c d u i 
+H0 c2 H3) in (let H5 \def H_x in (or3_ind (ex2 C (\lambda (d2: C).(getl i c2 
+(CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d2 d))) (ex4_3 C T A 
+(\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind 
+Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 
+d)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a1: A).(arity g d2 u2 
+(asucc g a1))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a1: A).(arity g d 
+u a1))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 
+(Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d)))) (arity 
+g c2 (TLRef i) a0) (\lambda (H6: (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 
+(Bind Abbr) u))) (\lambda (d2: C).(csuba g d2 d)))).(ex2_ind C (\lambda (d2: 
+C).(getl i c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d2 d)) 
+(arity g c2 (TLRef i) a0) (\lambda (x: C).(\lambda (H7: (getl i c2 (CHead x 
+(Bind Abbr) u))).(\lambda (H8: (csuba g x d)).(let H_x0 \def (csubv_getl_conf 
+c2 c H4 Abbr x u i H7) in (let H9 \def H_x0 in (ex2_3_ind B C T (\lambda (_: 
+B).(\lambda (d2: C).(\lambda (_: T).(csubv x d2)))) (\lambda (b2: B).(\lambda 
+(d2: C).(\lambda (v2: T).(getl i c (CHead d2 (Bind b2) v2))))) (arity g c2 
+(TLRef i) a0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda 
+(H10: (csubv x x1)).(\lambda (H11: (getl i c (CHead x1 (Bind x0) x2))).(let 
+H12 \def (eq_ind C (CHead d (Bind Abbr) u) (\lambda (c0: C).(getl i c c0)) H0 
+(CHead x1 (Bind x0) x2) (getl_mono c (CHead d (Bind Abbr) u) i H0 (CHead x1 
+(Bind x0) x2) H11)) in (let H13 \def (f_equal C C (\lambda (e: C).(match e 
+with [(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d 
+(Bind Abbr) u) (CHead x1 (Bind x0) x2) (getl_mono c (CHead d (Bind Abbr) u) i 
+H0 (CHead x1 (Bind x0) x2) H11)) in ((let H14 \def (f_equal C B (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow 
+(match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead 
+d (Bind Abbr) u) (CHead x1 (Bind x0) x2) (getl_mono c (CHead d (Bind Abbr) u) 
+i H0 (CHead x1 (Bind x0) x2) H11)) in ((let H15 \def (f_equal C T (\lambda 
+(e: C).(match e with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow 
+t0])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) (getl_mono c (CHead d 
+(Bind Abbr) u) i H0 (CHead x1 (Bind x0) x2) H11)) in (\lambda (H16: (eq B 
+Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def (eq_ind_r T x2 (\lambda 
+(t0: T).(getl i c (CHead x1 (Bind x0) t0))) H12 u H15) in (let H19 \def 
+(eq_ind_r C x1 (\lambda (c0: C).(getl i c (CHead c0 (Bind x0) u))) H18 d H17) 
+in (let H20 \def (eq_ind_r C x1 (\lambda (c0: C).(csubv x c0)) H10 d H17) in 
+(let H21 \def (eq_ind_r B x0 (\lambda (b: B).(getl i c (CHead d (Bind b) u))) 
+H19 Abbr H16) in (arity_abbr g c2 x u i H7 a0 (H2 x H8 H20))))))))) H14)) 
+H13)))))))) H9)))))) H6)) (\lambda (H6: (ex4_3 C T A (\lambda (d2: 
+C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abst) u2))))) 
+(\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d)))) (\lambda 
+(d2: C).(\lambda (u2: T).(\lambda (a1: A).(arity g d2 u2 (asucc g a1))))) 
+(\lambda (_: C).(\lambda (_: T).(\lambda (a1: A).(arity g d u 
+a1)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: 
+A).(getl i c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: 
+T).(\lambda (_: A).(csuba g d2 d)))) (\lambda (d2: C).(\lambda (u2: 
+T).(\lambda (a1: A).(arity g d2 u2 (asucc g a1))))) (\lambda (_: C).(\lambda 
+(_: T).(\lambda (a1: A).(arity g d u a1)))) (arity g c2 (TLRef i) a0) 
 (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H7: (getl i c2 
 (CHead x0 (Bind Abst) x1))).(\lambda (_: (csuba g x0 d)).(\lambda (H9: (arity 
-g x0 x1 (asucc g x2))).(\lambda (H10: (arity g d u x2)).(let TMP_100 \def 
-(TLRef i) in (let TMP_101 \def (arity_abst g c2 x0 x1 i H7 x2 H9) in (let 
-TMP_102 \def (arity_mono g d u x2 H10 a0 H1) in (arity_repl g c2 TMP_100 x2 
-TMP_101 a0 TMP_102))))))))))) in (ex4_3_ind C T A TMP_93 TMP_94 TMP_96 TMP_97 
-TMP_99 TMP_103 H6))))))))) in (let TMP_141 \def (\lambda (H6: (ex2_2 C T 
-(\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2)))) 
-(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))))).(let TMP_107 \def 
-(\lambda (d2: C).(\lambda (u2: T).(let TMP_105 \def (Bind Void) in (let 
-TMP_106 \def (CHead d2 TMP_105 u2) in (getl i c2 TMP_106))))) in (let TMP_108 
-\def (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))) in (let TMP_109 \def 
-(TLRef i) in (let TMP_110 \def (arity g c2 TMP_109 a0) in (let TMP_140 \def 
-(\lambda (x0: C).(\lambda (x1: T).(\lambda (H7: (getl i c2 (CHead x0 (Bind 
-Void) x1))).(\lambda (_: (csuba g x0 d)).(let H_x0 \def (csubv_getl_conf_void 
-c2 c H4 x0 x1 i H7) in (let H9 \def H_x0 in (let TMP_111 \def (\lambda (d2: 
-C).(\lambda (_: T).(csubv x0 d2))) in (let TMP_114 \def (\lambda (d2: 
-C).(\lambda (v2: T).(let TMP_112 \def (Bind Void) in (let TMP_113 \def (CHead 
-d2 TMP_112 v2) in (getl i c TMP_113))))) in (let TMP_115 \def (TLRef i) in 
-(let TMP_116 \def (arity g c2 TMP_115 a0) in (let TMP_139 \def (\lambda (x2: 
-C).(\lambda (x3: T).(\lambda (_: (csubv x0 x2)).(\lambda (H11: (getl i c 
-(CHead x2 (Bind Void) x3))).(let TMP_117 \def (Bind Abbr) in (let TMP_118 
-\def (CHead d TMP_117 u) in (let TMP_119 \def (\lambda (c0: C).(getl i c c0)) 
-in (let TMP_120 \def (Bind Void) in (let TMP_121 \def (CHead x2 TMP_120 x3) 
-in (let TMP_122 \def (Bind Abbr) in (let TMP_123 \def (CHead d TMP_122 u) in 
-(let TMP_124 \def (Bind Void) in (let TMP_125 \def (CHead x2 TMP_124 x3) in 
-(let TMP_126 \def (getl_mono c TMP_123 i H0 TMP_125 H11) in (let H12 \def 
-(eq_ind C TMP_118 TMP_119 H0 TMP_121 TMP_126) in (let TMP_127 \def (Bind 
-Abbr) in (let TMP_128 \def (CHead d TMP_127 u) in (let TMP_129 \def (\lambda 
-(ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _) 
-\Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr 
-\Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat 
-_) \Rightarrow False])])) in (let TMP_130 \def (Bind Void) in (let TMP_131 
-\def (CHead x2 TMP_130 x3) in (let TMP_132 \def (Bind Abbr) in (let TMP_133 
-\def (CHead d TMP_132 u) in (let TMP_134 \def (Bind Void) in (let TMP_135 
-\def (CHead x2 TMP_134 x3) in (let TMP_136 \def (getl_mono c TMP_133 i H0 
-TMP_135 H11) in (let H13 \def (eq_ind C TMP_128 TMP_129 I TMP_131 TMP_136) in 
-(let TMP_137 \def (TLRef i) in (let TMP_138 \def (arity g c2 TMP_137 a0) in 
-(False_ind TMP_138 H13))))))))))))))))))))))))))))) in (ex2_2_ind C T TMP_111 
-TMP_114 TMP_116 TMP_139 H9)))))))))))) in (ex2_2_ind C T TMP_107 TMP_108 
-TMP_110 TMP_140 H6))))))) in (or3_ind TMP_7 TMP_15 TMP_20 TMP_22 TMP_90 
-TMP_104 TMP_141 H5)))))))))))))))))))))))))))))) in (let TMP_260 \def 
-(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda 
-(H0: (getl i c (CHead d (Bind Abst) u))).(\lambda (a0: A).(\lambda (_: (arity 
-g d u (asucc g a0))).(\lambda (H2: ((\forall (c2: C).((csuba g c2 d) \to 
-((csubv c2 d) \to (arity g c2 u (asucc g a0))))))).(\lambda (c2: C).(\lambda 
-(H3: (csuba g c2 c)).(\lambda (H4: (csubv c2 c)).(let H_x \def 
-(csuba_getl_abst_rev g c d u i H0 c2 H3) in (let H5 \def H_x in (let TMP_145 
-\def (\lambda (d2: C).(let TMP_143 \def (Bind Abst) in (let TMP_144 \def 
-(CHead d2 TMP_143 u) in (getl i c2 TMP_144)))) in (let TMP_146 \def (\lambda 
-(d2: C).(csuba g d2 d)) in (let TMP_147 \def (ex2 C TMP_145 TMP_146) in (let 
-TMP_150 \def (\lambda (d2: C).(\lambda (u2: T).(let TMP_148 \def (Bind Void) 
-in (let TMP_149 \def (CHead d2 TMP_148 u2) in (getl i c2 TMP_149))))) in (let 
-TMP_151 \def (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))) in (let 
-TMP_152 \def (ex2_2 C T TMP_150 TMP_151) in (let TMP_153 \def (TLRef i) in 
-(let TMP_154 \def (arity g c2 TMP_153 a0) in (let TMP_222 \def (\lambda (H6: 
+g x0 x1 (asucc g x2))).(\lambda (H10: (arity g d u x2)).(arity_repl g c2 
+(TLRef i) x2 (arity_abst g c2 x0 x1 i H7 x2 H9) a0 (arity_mono g d u x2 H10 
+a0 H1))))))))) H6)) (\lambda (H6: (ex2_2 C T (\lambda (d2: C).(\lambda (u2: 
+T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: 
+T).(csuba g d2 d))))).(ex2_2_ind C T (\lambda (d2: C).(\lambda (u2: T).(getl 
+i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g 
+d2 d))) (arity g c2 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1: T).(\lambda 
+(H7: (getl i c2 (CHead x0 (Bind Void) x1))).(\lambda (_: (csuba g x0 d)).(let 
+H_x0 \def (csubv_getl_conf_void c2 c H4 x0 x1 i H7) in (let H9 \def H_x0 in 
+(ex2_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubv x0 d2))) (\lambda (d2: 
+C).(\lambda (v2: T).(getl i c (CHead d2 (Bind Void) v2)))) (arity g c2 (TLRef 
+i) a0) (\lambda (x2: C).(\lambda (x3: T).(\lambda (_: (csubv x0 x2)).(\lambda 
+(H11: (getl i c (CHead x2 (Bind Void) x3))).(let H12 \def (eq_ind C (CHead d 
+(Bind Abbr) u) (\lambda (c0: C).(getl i c c0)) H0 (CHead x2 (Bind Void) x3) 
+(getl_mono c (CHead d (Bind Abbr) u) i H0 (CHead x2 (Bind Void) x3) H11)) in 
+(let H13 \def (eq_ind C (CHead d (Bind Abbr) u) (\lambda (ee: C).(match ee 
+with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k with 
+[(Bind b) \Rightarrow (match b with [Abbr \Rightarrow True | Abst \Rightarrow 
+False | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead 
+x2 (Bind Void) x3) (getl_mono c (CHead d (Bind Abbr) u) i H0 (CHead x2 (Bind 
+Void) x3) H11)) in (False_ind (arity g c2 (TLRef i) a0) H13))))))) H9))))))) 
+H6)) H5)))))))))))))) (\lambda (c: C).(\lambda (d: C).(\lambda (u: 
+T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abst) 
+u))).(\lambda (a0: A).(\lambda (_: (arity g d u (asucc g a0))).(\lambda (H2: 
+((\forall (c2: C).((csuba g c2 d) \to ((csubv c2 d) \to (arity g c2 u (asucc 
+g a0))))))).(\lambda (c2: C).(\lambda (H3: (csuba g c2 c)).(\lambda (H4: 
+(csubv c2 c)).(let H_x \def (csuba_getl_abst_rev g c d u i H0 c2 H3) in (let 
+H5 \def H_x in (or_ind (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind 
+Abst) u))) (\lambda (d2: C).(csuba g d2 d))) (ex2_2 C T (\lambda (d2: 
+C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: 
+C).(\lambda (_: T).(csuba g d2 d)))) (arity g c2 (TLRef i) a0) (\lambda (H6: 
 (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: 
-C).(csuba g d2 d)))).(let TMP_157 \def (\lambda (d2: C).(let TMP_155 \def 
-(Bind Abst) in (let TMP_156 \def (CHead d2 TMP_155 u) in (getl i c2 
-TMP_156)))) in (let TMP_158 \def (\lambda (d2: C).(csuba g d2 d)) in (let 
-TMP_159 \def (TLRef i) in (let TMP_160 \def (arity g c2 TMP_159 a0) in (let 
-TMP_221 \def (\lambda (x: C).(\lambda (H7: (getl i c2 (CHead x (Bind Abst) 
-u))).(\lambda (H8: (csuba g x d)).(let H_x0 \def (csubv_getl_conf c2 c H4 
-Abst x u i H7) in (let H9 \def H_x0 in (let TMP_161 \def (\lambda (_: 
-B).(\lambda (d2: C).(\lambda (_: T).(csubv x d2)))) in (let TMP_164 \def 
-(\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(let TMP_162 \def (Bind 
-b2) in (let TMP_163 \def (CHead d2 TMP_162 v2) in (getl i c TMP_163)))))) in 
-(let TMP_165 \def (TLRef i) in (let TMP_166 \def (arity g c2 TMP_165 a0) in 
-(let TMP_220 \def (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda 
-(H10: (csubv x x1)).(\lambda (H11: (getl i c (CHead x1 (Bind x0) x2))).(let 
-TMP_167 \def (Bind Abst) in (let TMP_168 \def (CHead d TMP_167 u) in (let 
-TMP_169 \def (\lambda (c0: C).(getl i c c0)) in (let TMP_170 \def (Bind x0) 
-in (let TMP_171 \def (CHead x1 TMP_170 x2) in (let TMP_172 \def (Bind Abst) 
-in (let TMP_173 \def (CHead d TMP_172 u) in (let TMP_174 \def (Bind x0) in 
-(let TMP_175 \def (CHead x1 TMP_174 x2) in (let TMP_176 \def (getl_mono c 
-TMP_173 i H0 TMP_175 H11) in (let H12 \def (eq_ind C TMP_168 TMP_169 H0 
-TMP_171 TMP_176) in (let TMP_177 \def (\lambda (e: C).(match e with [(CSort 
-_) \Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) in (let TMP_178 \def 
-(Bind Abst) in (let TMP_179 \def (CHead d TMP_178 u) in (let TMP_180 \def 
-(Bind x0) in (let TMP_181 \def (CHead x1 TMP_180 x2) in (let TMP_182 \def 
-(Bind Abst) in (let TMP_183 \def (CHead d TMP_182 u) in (let TMP_184 \def 
-(Bind x0) in (let TMP_185 \def (CHead x1 TMP_184 x2) in (let TMP_186 \def 
-(getl_mono c TMP_183 i H0 TMP_185 H11) in (let H13 \def (f_equal C C TMP_177 
-TMP_179 TMP_181 TMP_186) in (let TMP_187 \def (\lambda (e: C).(match e with 
-[(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k with [(Bind 
-b) \Rightarrow b | (Flat _) \Rightarrow Abst])])) in (let TMP_188 \def (Bind 
-Abst) in (let TMP_189 \def (CHead d TMP_188 u) in (let TMP_190 \def (Bind x0) 
-in (let TMP_191 \def (CHead x1 TMP_190 x2) in (let TMP_192 \def (Bind Abst) 
-in (let TMP_193 \def (CHead d TMP_192 u) in (let TMP_194 \def (Bind x0) in 
-(let TMP_195 \def (CHead x1 TMP_194 x2) in (let TMP_196 \def (getl_mono c 
-TMP_193 i H0 TMP_195 H11) in (let H14 \def (f_equal C B TMP_187 TMP_189 
-TMP_191 TMP_196) in (let TMP_197 \def (\lambda (e: C).(match e with [(CSort 
-_) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) in (let TMP_198 \def 
-(Bind Abst) in (let TMP_199 \def (CHead d TMP_198 u) in (let TMP_200 \def 
-(Bind x0) in (let TMP_201 \def (CHead x1 TMP_200 x2) in (let TMP_202 \def 
-(Bind Abst) in (let TMP_203 \def (CHead d TMP_202 u) in (let TMP_204 \def 
-(Bind x0) in (let TMP_205 \def (CHead x1 TMP_204 x2) in (let TMP_206 \def 
-(getl_mono c TMP_203 i H0 TMP_205 H11) in (let H15 \def (f_equal C T TMP_197 
-TMP_199 TMP_201 TMP_206) in (let TMP_218 \def (\lambda (H16: (eq B Abst 
-x0)).(\lambda (H17: (eq C d x1)).(let TMP_209 \def (\lambda (t0: T).(let 
-TMP_207 \def (Bind x0) in (let TMP_208 \def (CHead x1 TMP_207 t0) in (getl i 
-c TMP_208)))) in (let H18 \def (eq_ind_r T x2 TMP_209 H12 u H15) in (let 
-TMP_212 \def (\lambda (c0: C).(let TMP_210 \def (Bind x0) in (let TMP_211 
-\def (CHead c0 TMP_210 u) in (getl i c TMP_211)))) in (let H19 \def (eq_ind_r 
-C x1 TMP_212 H18 d H17) in (let TMP_213 \def (\lambda (c0: C).(csubv x c0)) 
-in (let H20 \def (eq_ind_r C x1 TMP_213 H10 d H17) in (let TMP_216 \def 
-(\lambda (b: B).(let TMP_214 \def (Bind b) in (let TMP_215 \def (CHead d 
-TMP_214 u) in (getl i c TMP_215)))) in (let H21 \def (eq_ind_r B x0 TMP_216 
-H19 Abst H16) in (let TMP_217 \def (H2 x H8 H20) in (arity_abst g c2 x u i H7 
-a0 TMP_217)))))))))))) in (let TMP_219 \def (TMP_218 H14) in (TMP_219 
-H13)))))))))))))))))))))))))))))))))))))))))))))))))))) in (ex2_3_ind B C T 
-TMP_161 TMP_164 TMP_166 TMP_220 H9))))))))))) in (ex2_ind C TMP_157 TMP_158 
-TMP_160 TMP_221 H6))))))) in (let TMP_259 \def (\lambda (H6: (ex2_2 C T 
-(\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2)))) 
-(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))))).(let TMP_225 \def 
-(\lambda (d2: C).(\lambda (u2: T).(let TMP_223 \def (Bind Void) in (let 
-TMP_224 \def (CHead d2 TMP_223 u2) in (getl i c2 TMP_224))))) in (let TMP_226 
-\def (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))) in (let TMP_227 \def 
-(TLRef i) in (let TMP_228 \def (arity g c2 TMP_227 a0) in (let TMP_258 \def 
-(\lambda (x0: C).(\lambda (x1: T).(\lambda (H7: (getl i c2 (CHead x0 (Bind 
-Void) x1))).(\lambda (_: (csuba g x0 d)).(let H_x0 \def (csubv_getl_conf_void 
-c2 c H4 x0 x1 i H7) in (let H9 \def H_x0 in (let TMP_229 \def (\lambda (d2: 
-C).(\lambda (_: T).(csubv x0 d2))) in (let TMP_232 \def (\lambda (d2: 
-C).(\lambda (v2: T).(let TMP_230 \def (Bind Void) in (let TMP_231 \def (CHead 
-d2 TMP_230 v2) in (getl i c TMP_231))))) in (let TMP_233 \def (TLRef i) in 
-(let TMP_234 \def (arity g c2 TMP_233 a0) in (let TMP_257 \def (\lambda (x2: 
-C).(\lambda (x3: T).(\lambda (_: (csubv x0 x2)).(\lambda (H11: (getl i c 
-(CHead x2 (Bind Void) x3))).(let TMP_235 \def (Bind Abst) in (let TMP_236 
-\def (CHead d TMP_235 u) in (let TMP_237 \def (\lambda (c0: C).(getl i c c0)) 
-in (let TMP_238 \def (Bind Void) in (let TMP_239 \def (CHead x2 TMP_238 x3) 
-in (let TMP_240 \def (Bind Abst) in (let TMP_241 \def (CHead d TMP_240 u) in 
-(let TMP_242 \def (Bind Void) in (let TMP_243 \def (CHead x2 TMP_242 x3) in 
-(let TMP_244 \def (getl_mono c TMP_241 i H0 TMP_243 H11) in (let H12 \def 
-(eq_ind C TMP_236 TMP_237 H0 TMP_239 TMP_244) in (let TMP_245 \def (Bind 
-Abst) in (let TMP_246 \def (CHead d TMP_245 u) in (let TMP_247 \def (\lambda 
-(ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _) 
-\Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr 
-\Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat 
-_) \Rightarrow False])])) in (let TMP_248 \def (Bind Void) in (let TMP_249 
-\def (CHead x2 TMP_248 x3) in (let TMP_250 \def (Bind Abst) in (let TMP_251 
-\def (CHead d TMP_250 u) in (let TMP_252 \def (Bind Void) in (let TMP_253 
-\def (CHead x2 TMP_252 x3) in (let TMP_254 \def (getl_mono c TMP_251 i H0 
-TMP_253 H11) in (let H13 \def (eq_ind C TMP_246 TMP_247 I TMP_249 TMP_254) in 
-(let TMP_255 \def (TLRef i) in (let TMP_256 \def (arity g c2 TMP_255 a0) in 
-(False_ind TMP_256 H13))))))))))))))))))))))))))))) in (ex2_2_ind C T TMP_229 
-TMP_232 TMP_234 TMP_257 H9)))))))))))) in (ex2_2_ind C T TMP_225 TMP_226 
-TMP_228 TMP_258 H6))))))) in (or_ind TMP_147 TMP_152 TMP_154 TMP_222 TMP_259 
-H5)))))))))))))))))))))))) in (let TMP_268 \def (\lambda (b: B).(\lambda (H0: 
-(not (eq B b Abst))).(\lambda (c: C).(\lambda (u: T).(\lambda (a1: 
-A).(\lambda (_: (arity g c u a1)).(\lambda (H2: ((\forall (c2: C).((csuba g 
-c2 c) \to ((csubv c2 c) \to (arity g c2 u a1)))))).(\lambda (t0: T).(\lambda 
-(a2: A).(\lambda (_: (arity g (CHead c (Bind b) u) t0 a2)).(\lambda (H4: 
-((\forall (c2: C).((csuba g c2 (CHead c (Bind b) u)) \to ((csubv c2 (CHead c 
-(Bind b) u)) \to (arity g c2 t0 a2)))))).(\lambda (c2: C).(\lambda (H5: 
-(csuba g c2 c)).(\lambda (H6: (csubv c2 c)).(let TMP_261 \def (H2 c2 H5 H6) 
-in (let TMP_262 \def (Bind b) in (let TMP_263 \def (CHead c2 TMP_262 u) in 
-(let TMP_264 \def (Bind b) in (let TMP_265 \def (csuba_head g c2 c H5 TMP_264 
-u) in (let TMP_266 \def (csubv_bind_same c2 c H6 b u u) in (let TMP_267 \def 
-(H4 TMP_263 TMP_265 TMP_266) in (arity_bind g b H0 c2 u a1 TMP_261 t0 a2 
-TMP_267)))))))))))))))))))))) in (let TMP_276 \def (\lambda (c: C).(\lambda 
-(u: T).(\lambda (a1: A).(\lambda (_: (arity g c u (asucc g a1))).(\lambda 
+C).(csuba g d2 d)))).(ex2_ind C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind 
+Abst) u))) (\lambda (d2: C).(csuba g d2 d)) (arity g c2 (TLRef i) a0) 
+(\lambda (x: C).(\lambda (H7: (getl i c2 (CHead x (Bind Abst) u))).(\lambda 
+(H8: (csuba g x d)).(let H_x0 \def (csubv_getl_conf c2 c H4 Abst x u i H7) in 
+(let H9 \def H_x0 in (ex2_3_ind B C T (\lambda (_: B).(\lambda (d2: 
+C).(\lambda (_: T).(csubv x d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda 
+(v2: T).(getl i c (CHead d2 (Bind b2) v2))))) (arity g c2 (TLRef i) a0) 
+(\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H10: (csubv x 
+x1)).(\lambda (H11: (getl i c (CHead x1 (Bind x0) x2))).(let H12 \def (eq_ind 
+C (CHead d (Bind Abst) u) (\lambda (c0: C).(getl i c c0)) H0 (CHead x1 (Bind 
+x0) x2) (getl_mono c (CHead d (Bind Abst) u) i H0 (CHead x1 (Bind x0) x2) 
+H11)) in (let H13 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abst) u) 
+(CHead x1 (Bind x0) x2) (getl_mono c (CHead d (Bind Abst) u) i H0 (CHead x1 
+(Bind x0) x2) H11)) in ((let H14 \def (f_equal C B (\lambda (e: C).(match e 
+with [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k with 
+[(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abst])])) (CHead d (Bind Abst) 
+u) (CHead x1 (Bind x0) x2) (getl_mono c (CHead d (Bind Abst) u) i H0 (CHead 
+x1 (Bind x0) x2) H11)) in ((let H15 \def (f_equal C T (\lambda (e: C).(match 
+e with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d 
+(Bind Abst) u) (CHead x1 (Bind x0) x2) (getl_mono c (CHead d (Bind Abst) u) i 
+H0 (CHead x1 (Bind x0) x2) H11)) in (\lambda (H16: (eq B Abst x0)).(\lambda 
+(H17: (eq C d x1)).(let H18 \def (eq_ind_r T x2 (\lambda (t0: T).(getl i c 
+(CHead x1 (Bind x0) t0))) H12 u H15) in (let H19 \def (eq_ind_r C x1 (\lambda 
+(c0: C).(getl i c (CHead c0 (Bind x0) u))) H18 d H17) in (let H20 \def 
+(eq_ind_r C x1 (\lambda (c0: C).(csubv x c0)) H10 d H17) in (let H21 \def 
+(eq_ind_r B x0 (\lambda (b: B).(getl i c (CHead d (Bind b) u))) H19 Abst H16) 
+in (arity_abst g c2 x u i H7 a0 (H2 x H8 H20))))))))) H14)) H13)))))))) 
+H9)))))) H6)) (\lambda (H6: (ex2_2 C T (\lambda (d2: C).(\lambda (u2: 
+T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: 
+T).(csuba g d2 d))))).(ex2_2_ind C T (\lambda (d2: C).(\lambda (u2: T).(getl 
+i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g 
+d2 d))) (arity g c2 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1: T).(\lambda 
+(H7: (getl i c2 (CHead x0 (Bind Void) x1))).(\lambda (_: (csuba g x0 d)).(let 
+H_x0 \def (csubv_getl_conf_void c2 c H4 x0 x1 i H7) in (let H9 \def H_x0 in 
+(ex2_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubv x0 d2))) (\lambda (d2: 
+C).(\lambda (v2: T).(getl i c (CHead d2 (Bind Void) v2)))) (arity g c2 (TLRef 
+i) a0) (\lambda (x2: C).(\lambda (x3: T).(\lambda (_: (csubv x0 x2)).(\lambda 
+(H11: (getl i c (CHead x2 (Bind Void) x3))).(let H12 \def (eq_ind C (CHead d 
+(Bind Abst) u) (\lambda (c0: C).(getl i c c0)) H0 (CHead x2 (Bind Void) x3) 
+(getl_mono c (CHead d (Bind Abst) u) i H0 (CHead x2 (Bind Void) x3) H11)) in 
+(let H13 \def (eq_ind C (CHead d (Bind Abst) u) (\lambda (ee: C).(match ee 
+with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k with 
+[(Bind b) \Rightarrow (match b with [Abbr \Rightarrow False | Abst 
+\Rightarrow True | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) 
+I (CHead x2 (Bind Void) x3) (getl_mono c (CHead d (Bind Abst) u) i H0 (CHead 
+x2 (Bind Void) x3) H11)) in (False_ind (arity g c2 (TLRef i) a0) H13))))))) 
+H9))))))) H6)) H5)))))))))))))) (\lambda (b: B).(\lambda (H0: (not (eq B b 
+Abst))).(\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity 
+g c u a1)).(\lambda (H2: ((\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c) 
+\to (arity g c2 u a1)))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: 
+(arity g (CHead c (Bind b) u) t0 a2)).(\lambda (H4: ((\forall (c2: C).((csuba 
+g c2 (CHead c (Bind b) u)) \to ((csubv c2 (CHead c (Bind b) u)) \to (arity g 
+c2 t0 a2)))))).(\lambda (c2: C).(\lambda (H5: (csuba g c2 c)).(\lambda (H6: 
+(csubv c2 c)).(arity_bind g b H0 c2 u a1 (H2 c2 H5 H6) t0 a2 (H4 (CHead c2 
+(Bind b) u) (csuba_head g c2 c H5 (Bind b) u) (csubv_bind_same c2 c H6 b u 
+u))))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda 
+(_: (arity g c u (asucc g a1))).(\lambda (H1: ((\forall (c2: C).((csuba g c2 
+c) \to ((csubv c2 c) \to (arity g c2 u (asucc g a1))))))).(\lambda (t0: 
+T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c (Bind Abst) u) t0 
+a2)).(\lambda (H3: ((\forall (c2: C).((csuba g c2 (CHead c (Bind Abst) u)) 
+\to ((csubv c2 (CHead c (Bind Abst) u)) \to (arity g c2 t0 a2)))))).(\lambda 
+(c2: C).(\lambda (H4: (csuba g c2 c)).(\lambda (H5: (csubv c2 c)).(arity_head 
+g c2 u a1 (H1 c2 H4 H5) t0 a2 (H3 (CHead c2 (Bind Abst) u) (csuba_head g c2 c 
+H4 (Bind Abst) u) (csubv_bind_same c2 c H5 Abst u u))))))))))))))) (\lambda 
+(c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u 
+a1)).(\lambda (H1: ((\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to 
+(arity g c2 u a1)))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity 
+g c t0 (AHead a1 a2))).(\lambda (H3: ((\forall (c2: C).((csuba g c2 c) \to 
+((csubv c2 c) \to (arity g c2 t0 (AHead a1 a2))))))).(\lambda (c2: 
+C).(\lambda (H4: (csuba g c2 c)).(\lambda (H5: (csubv c2 c)).(arity_appl g c2 
+u a1 (H1 c2 H4 H5) t0 a2 (H3 c2 H4 H5)))))))))))))) (\lambda (c: C).(\lambda 
+(u: T).(\lambda (a0: A).(\lambda (_: (arity g c u (asucc g a0))).(\lambda 
 (H1: ((\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 u 
-(asucc g a1))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g 
-(CHead c (Bind Abst) u) t0 a2)).(\lambda (H3: ((\forall (c2: C).((csuba g c2 
-(CHead c (Bind Abst) u)) \to ((csubv c2 (CHead c (Bind Abst) u)) \to (arity g 
-c2 t0 a2)))))).(\lambda (c2: C).(\lambda (H4: (csuba g c2 c)).(\lambda (H5: 
-(csubv c2 c)).(let TMP_269 \def (H1 c2 H4 H5) in (let TMP_270 \def (Bind 
-Abst) in (let TMP_271 \def (CHead c2 TMP_270 u) in (let TMP_272 \def (Bind 
-Abst) in (let TMP_273 \def (csuba_head g c2 c H4 TMP_272 u) in (let TMP_274 
-\def (csubv_bind_same c2 c H5 Abst u u) in (let TMP_275 \def (H3 TMP_271 
-TMP_273 TMP_274) in (arity_head g c2 u a1 TMP_269 t0 a2 
-TMP_275)))))))))))))))))))) in (let TMP_279 \def (\lambda (c: C).(\lambda (u: 
-T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H1: ((\forall 
-(c2: C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 u a1)))))).(\lambda 
-(t0: T).(\lambda (a2: A).(\lambda (_: (arity g c t0 (AHead a1 a2))).(\lambda 
+(asucc g a0))))))).(\lambda (t0: T).(\lambda (_: (arity g c t0 a0)).(\lambda 
 (H3: ((\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 t0 
-(AHead a1 a2))))))).(\lambda (c2: C).(\lambda (H4: (csuba g c2 c)).(\lambda 
-(H5: (csubv c2 c)).(let TMP_277 \def (H1 c2 H4 H5) in (let TMP_278 \def (H3 
-c2 H4 H5) in (arity_appl g c2 u a1 TMP_277 t0 a2 TMP_278))))))))))))))) in 
-(let TMP_282 \def (\lambda (c: C).(\lambda (u: T).(\lambda (a0: A).(\lambda 
-(_: (arity g c u (asucc g a0))).(\lambda (H1: ((\forall (c2: C).((csuba g c2 
-c) \to ((csubv c2 c) \to (arity g c2 u (asucc g a0))))))).(\lambda (t0: 
-T).(\lambda (_: (arity g c t0 a0)).(\lambda (H3: ((\forall (c2: C).((csuba g 
-c2 c) \to ((csubv c2 c) \to (arity g c2 t0 a0)))))).(\lambda (c2: C).(\lambda 
-(H4: (csuba g c2 c)).(\lambda (H5: (csubv c2 c)).(let TMP_280 \def (H1 c2 H4 
-H5) in (let TMP_281 \def (H3 c2 H4 H5) in (arity_cast g c2 u a0 TMP_280 t0 
-TMP_281)))))))))))))) in (let TMP_284 \def (\lambda (c: C).(\lambda (t0: 
-T).(\lambda (a1: A).(\lambda (_: (arity g c t0 a1)).(\lambda (H1: ((\forall 
-(c2: C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 t0 
-a1)))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2: 
-C).(\lambda (H3: (csuba g c2 c)).(\lambda (H4: (csubv c2 c)).(let TMP_283 
-\def (H1 c2 H3 H4) in (arity_repl g c2 t0 a1 TMP_283 a2 H2)))))))))))) in 
-(arity_ind g TMP_1 TMP_2 TMP_142 TMP_260 TMP_268 TMP_276 TMP_279 TMP_282 
-TMP_284 c1 t a H)))))))))))))).
+a0)))))).(\lambda (c2: C).(\lambda (H4: (csuba g c2 c)).(\lambda (H5: (csubv 
+c2 c)).(arity_cast g c2 u a0 (H1 c2 H4 H5) t0 (H3 c2 H4 H5))))))))))))) 
+(\lambda (c: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda (_: (arity g c t0 
+a1)).(\lambda (H1: ((\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to 
+(arity g c2 t0 a1)))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 
+a2)).(\lambda (c2: C).(\lambda (H3: (csuba g c2 c)).(\lambda (H4: (csubv c2 
+c)).(arity_repl g c2 t0 a1 (H1 c2 H3 H4) a2 H2))))))))))) c1 t a H))))).
 
 theorem arity_appls_appl:
  \forall (g: G).(\forall (c: C).(\forall (v: T).(\forall (a1: A).((arity g c 
@@ -429,52 +290,30 @@ T).(\forall (vs: TList).(\forall (a2: A).((arity g c (THeads (Flat Appl) vs
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (v: T).(\lambda (a1: A).(\lambda (H: 
 (arity g c v a1)).(\lambda (u: T).(\lambda (H0: (arity g c u (asucc g 
-a1))).(\lambda (t: T).(\lambda (vs: TList).(let TMP_7 \def (\lambda (t0: 
+a1))).(\lambda (t: T).(\lambda (vs: TList).(TList_ind (\lambda (t0: 
 TList).(\forall (a2: A).((arity g c (THeads (Flat Appl) t0 (THead (Bind Abbr) 
-v t)) a2) \to (let TMP_1 \def (Flat Appl) in (let TMP_2 \def (Flat Appl) in 
-(let TMP_3 \def (Bind Abst) in (let TMP_4 \def (THead TMP_3 u t) in (let 
-TMP_5 \def (THead TMP_2 v TMP_4) in (let TMP_6 \def (THeads TMP_1 t0 TMP_5) 
-in (arity g c TMP_6 a2)))))))))) in (let TMP_30 \def (\lambda (a2: 
-A).(\lambda (H1: (arity g c (THead (Bind Abbr) v t) a2)).(let H_x \def 
-(arity_gen_bind Abbr not_abbr_abst g c v t a2 H1) in (let H2 \def H_x in (let 
-TMP_8 \def (\lambda (a3: A).(arity g c v a3)) in (let TMP_11 \def (\lambda 
-(_: A).(let TMP_9 \def (Bind Abbr) in (let TMP_10 \def (CHead c TMP_9 v) in 
-(arity g TMP_10 t a2)))) in (let TMP_12 \def (Flat Appl) in (let TMP_13 \def 
-(Bind Abst) in (let TMP_14 \def (THead TMP_13 u t) in (let TMP_15 \def (THead 
-TMP_12 v TMP_14) in (let TMP_16 \def (arity g c TMP_15 a2) in (let TMP_29 
-\def (\lambda (x: A).(\lambda (_: (arity g c v x)).(\lambda (H4: (arity g 
-(CHead c (Bind Abbr) v) t a2)).(let TMP_17 \def (Bind Abst) in (let TMP_18 
-\def (THead TMP_17 u t) in (let TMP_19 \def (Bind Abbr) in (let TMP_20 \def 
-(CHead c TMP_19 v) in (let TMP_21 \def (Bind Abst) in (let TMP_22 \def (CHead 
-c TMP_21 u) in (let TMP_23 \def (csuba_refl g c) in (let TMP_24 \def 
-(csuba_abst g c c TMP_23 u a1 H0 v H) in (let TMP_25 \def (csubv_refl c) in 
-(let TMP_26 \def (csubv_bind c c TMP_25 Abst not_abst_void Abbr u v) in (let 
-TMP_27 \def (csuba_arity_rev g TMP_20 t a2 H4 TMP_22 TMP_24 TMP_26) in (let 
-TMP_28 \def (arity_head g c u a1 H0 t a2 TMP_27) in (arity_appl g c v a1 H 
-TMP_18 a2 TMP_28)))))))))))))))) in (ex2_ind A TMP_8 TMP_11 TMP_16 TMP_29 
-H2))))))))))))) in (let TMP_60 \def (\lambda (t0: T).(\lambda (t1: 
-TList).(\lambda (H1: ((\forall (a2: A).((arity g c (THeads (Flat Appl) t1 
-(THead (Bind Abbr) v t)) a2) \to (arity g c (THeads (Flat Appl) t1 (THead 
-(Flat Appl) v (THead (Bind Abst) u t))) a2))))).(\lambda (a2: A).(\lambda 
-(H2: (arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 (THead (Bind 
-Abbr) v t))) a2)).(let TMP_31 \def (Flat Appl) in (let TMP_32 \def (Bind 
-Abbr) in (let TMP_33 \def (THead TMP_32 v t) in (let TMP_34 \def (THeads 
-TMP_31 t1 TMP_33) in (let H3 \def (arity_gen_appl g c t0 TMP_34 a2 H2) in 
-(let TMP_35 \def (\lambda (a3: A).(arity g c t0 a3)) in (let TMP_41 \def 
-(\lambda (a3: A).(let TMP_36 \def (Flat Appl) in (let TMP_37 \def (Bind Abbr) 
-in (let TMP_38 \def (THead TMP_37 v t) in (let TMP_39 \def (THeads TMP_36 t1 
-TMP_38) in (let TMP_40 \def (AHead a3 a2) in (arity g c TMP_39 TMP_40))))))) 
-in (let TMP_42 \def (Flat Appl) in (let TMP_43 \def (Flat Appl) in (let 
-TMP_44 \def (Flat Appl) in (let TMP_45 \def (Bind Abst) in (let TMP_46 \def 
-(THead TMP_45 u t) in (let TMP_47 \def (THead TMP_44 v TMP_46) in (let TMP_48 
-\def (THeads TMP_43 t1 TMP_47) in (let TMP_49 \def (THead TMP_42 t0 TMP_48) 
-in (let TMP_50 \def (arity g c TMP_49 a2) in (let TMP_59 \def (\lambda (x: 
-A).(\lambda (H4: (arity g c t0 x)).(\lambda (H5: (arity g c (THeads (Flat 
-Appl) t1 (THead (Bind Abbr) v t)) (AHead x a2))).(let TMP_51 \def (Flat Appl) 
-in (let TMP_52 \def (Flat Appl) in (let TMP_53 \def (Bind Abst) in (let 
-TMP_54 \def (THead TMP_53 u t) in (let TMP_55 \def (THead TMP_52 v TMP_54) in 
-(let TMP_56 \def (THeads TMP_51 t1 TMP_55) in (let TMP_57 \def (AHead x a2) 
-in (let TMP_58 \def (H1 TMP_57 H5) in (arity_appl g c t0 x H4 TMP_56 a2 
-TMP_58)))))))))))) in (ex2_ind A TMP_35 TMP_41 TMP_50 TMP_59 
-H3))))))))))))))))))))))) in (TList_ind TMP_7 TMP_30 TMP_60 vs)))))))))))).
+v t)) a2) \to (arity g c (THeads (Flat Appl) t0 (THead (Flat Appl) v (THead 
+(Bind Abst) u t))) a2)))) (\lambda (a2: A).(\lambda (H1: (arity g c (THead 
+(Bind Abbr) v t) a2)).(let H_x \def (arity_gen_bind Abbr not_abbr_abst g c v 
+t a2 H1) in (let H2 \def H_x in (ex2_ind A (\lambda (a3: A).(arity g c v a3)) 
+(\lambda (_: A).(arity g (CHead c (Bind Abbr) v) t a2)) (arity g c (THead 
+(Flat Appl) v (THead (Bind Abst) u t)) a2) (\lambda (x: A).(\lambda (_: 
+(arity g c v x)).(\lambda (H4: (arity g (CHead c (Bind Abbr) v) t 
+a2)).(arity_appl g c v a1 H (THead (Bind Abst) u t) a2 (arity_head g c u a1 
+H0 t a2 (csuba_arity_rev g (CHead c (Bind Abbr) v) t a2 H4 (CHead c (Bind 
+Abst) u) (csuba_abst g c c (csuba_refl g c) u a1 H0 v H) (csubv_bind c c 
+(csubv_refl c) Abst not_abst_void Abbr u v))))))) H2))))) (\lambda (t0: 
+T).(\lambda (t1: TList).(\lambda (H1: ((\forall (a2: A).((arity g c (THeads 
+(Flat Appl) t1 (THead (Bind Abbr) v t)) a2) \to (arity g c (THeads (Flat 
+Appl) t1 (THead (Flat Appl) v (THead (Bind Abst) u t))) a2))))).(\lambda (a2: 
+A).(\lambda (H2: (arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 
+(THead (Bind Abbr) v t))) a2)).(let H3 \def (arity_gen_appl g c t0 (THeads 
+(Flat Appl) t1 (THead (Bind Abbr) v t)) a2 H2) in (ex2_ind A (\lambda (a3: 
+A).(arity g c t0 a3)) (\lambda (a3: A).(arity g c (THeads (Flat Appl) t1 
+(THead (Bind Abbr) v t)) (AHead a3 a2))) (arity g c (THead (Flat Appl) t0 
+(THeads (Flat Appl) t1 (THead (Flat Appl) v (THead (Bind Abst) u t)))) a2) 
+(\lambda (x: A).(\lambda (H4: (arity g c t0 x)).(\lambda (H5: (arity g c 
+(THeads (Flat Appl) t1 (THead (Bind Abbr) v t)) (AHead x a2))).(arity_appl g 
+c t0 x H4 (THeads (Flat Appl) t1 (THead (Flat Appl) v (THead (Bind Abst) u 
+t))) a2 (H1 (AHead x a2) H5))))) H3))))))) vs))))))))).