- \lambda (i: nat).(let TMP_1 \def (\lambda (n: nat).(\forall (c1: C).(\forall
-(c3: C).((getl n c1 c3) \to (\forall (c2: C).((clear c1 c2) \to (getl n c2
-c3))))))) in (let TMP_20 \def (\lambda (c1: C).(\lambda (c3: C).(\lambda (H:
-(getl O c1 c3)).(\lambda (c2: C).(\lambda (H0: (clear c1 c2)).(let TMP_2 \def
-(\lambda (c: C).(getl O c c3)) in (let TMP_3 \def (getl_gen_O c1 c3 H) in
-(let H1 \def (clear_gen_all c1 c3 TMP_3) in (let TMP_6 \def (\lambda (b:
-B).(\lambda (e: C).(\lambda (u: T).(let TMP_4 \def (Bind b) in (let TMP_5
-\def (CHead e TMP_4 u) in (eq C c3 TMP_5)))))) in (let TMP_7 \def (getl O c3
-c3) in (let TMP_16 \def (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2:
-T).(\lambda (H2: (eq C c3 (CHead x1 (Bind x0) x2))).(let TMP_8 \def (\lambda
-(c: C).(clear c1 c)) in (let TMP_9 \def (getl_gen_O c1 c3 H) in (let TMP_10
-\def (Bind x0) in (let TMP_11 \def (CHead x1 TMP_10 x2) in (let H3 \def
-(eq_ind C c3 TMP_8 TMP_9 TMP_11 H2) in (let TMP_12 \def (Bind x0) in (let
-TMP_13 \def (CHead x1 TMP_12 x2) in (let TMP_14 \def (\lambda (c: C).(getl O
-c c)) in (let TMP_15 \def (getl_refl x0 x1 x2) in (eq_ind_r C TMP_13 TMP_14
-TMP_15 c3 H2)))))))))))))) in (let TMP_17 \def (ex_3_ind B C T TMP_6 TMP_7
-TMP_16 H1) in (let TMP_18 \def (getl_gen_O c1 c3 H) in (let TMP_19 \def
-(clear_mono c1 c3 TMP_18 c2 H0) in (eq_ind C c3 TMP_2 TMP_17 c2
-TMP_19))))))))))))))) in (let TMP_44 \def (\lambda (n: nat).(\lambda (_:
-((\forall (c1: C).(\forall (c3: C).((getl n c1 c3) \to (\forall (c2:
-C).((clear c1 c2) \to (getl n c2 c3)))))))).(\lambda (c1: C).(let TMP_22 \def
-(\lambda (c: C).(\forall (c3: C).((getl (S n) c c3) \to (\forall (c2:
-C).((clear c c2) \to (let TMP_21 \def (S n) in (getl TMP_21 c2 c3))))))) in
-(let TMP_26 \def (\lambda (n0: nat).(\lambda (c3: C).(\lambda (H0: (getl (S
-n) (CSort n0) c3)).(\lambda (c2: C).(\lambda (_: (clear (CSort n0) c2)).(let
-TMP_23 \def (S n) in (let TMP_24 \def (S n) in (let TMP_25 \def (getl TMP_24
-c2 c3) in (getl_gen_sort n0 TMP_23 c3 H0 TMP_25))))))))) in (let TMP_43 \def
-(\lambda (c: C).(\lambda (H0: ((\forall (c3: C).((getl (S n) c c3) \to
-(\forall (c2: C).((clear c c2) \to (getl (S n) c2 c3))))))).(\lambda (k:
-K).(\lambda (t: T).(\lambda (c3: C).(\lambda (H1: (getl (S n) (CHead c k t)
-c3)).(\lambda (c2: C).(\lambda (H2: (clear (CHead c k t) c2)).(let TMP_28
-\def (\lambda (k0: K).((getl (S n) (CHead c k0 t) c3) \to ((clear (CHead c k0
-t) c2) \to (let TMP_27 \def (S n) in (getl TMP_27 c2 c3))))) in (let TMP_38
-\def (\lambda (b: B).(\lambda (H3: (getl (S n) (CHead c (Bind b) t)
-c3)).(\lambda (H4: (clear (CHead c (Bind b) t) c2)).(let TMP_29 \def (Bind b)
-in (let TMP_30 \def (CHead c TMP_29 t) in (let TMP_32 \def (\lambda (c0:
-C).(let TMP_31 \def (S n) in (getl TMP_31 c0 c3))) in (let TMP_33 \def (Bind
-b) in (let TMP_34 \def (Bind b) in (let TMP_35 \def (getl_gen_S TMP_34 c c3 t
-n H3) in (let TMP_36 \def (getl_head TMP_33 n c c3 TMP_35 t) in (let TMP_37
-\def (clear_gen_bind b c c2 t H4) in (eq_ind_r C TMP_30 TMP_32 TMP_36 c2
-TMP_37)))))))))))) in (let TMP_42 \def (\lambda (f: F).(\lambda (H3: (getl (S
-n) (CHead c (Flat f) t) c3)).(\lambda (H4: (clear (CHead c (Flat f) t)
-c2)).(let TMP_39 \def (Flat f) in (let TMP_40 \def (getl_gen_S TMP_39 c c3 t
-n H3) in (let TMP_41 \def (clear_gen_flat f c c2 t H4) in (H0 c3 TMP_40 c2
-TMP_41))))))) in (K_ind TMP_28 TMP_38 TMP_42 k H1 H2)))))))))))) in (C_ind
-TMP_22 TMP_26 TMP_43 c1))))))) in (nat_ind TMP_1 TMP_20 TMP_44 i)))).
+ \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (c3:
+C).((getl n c1 c3) \to (\forall (c2: C).((clear c1 c2) \to (getl n c2
+c3))))))) (\lambda (c1: C).(\lambda (c3: C).(\lambda (H: (getl O c1
+c3)).(\lambda (c2: C).(\lambda (H0: (clear c1 c2)).(eq_ind C c3 (\lambda (c:
+C).(getl O c c3)) (let H1 \def (clear_gen_all c1 c3 (getl_gen_O c1 c3 H)) in
+(ex_3_ind B C T (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(eq C c3
+(CHead e (Bind b) u))))) (getl O c3 c3) (\lambda (x0: B).(\lambda (x1:
+C).(\lambda (x2: T).(\lambda (H2: (eq C c3 (CHead x1 (Bind x0) x2))).(let H3
+\def (eq_ind C c3 (\lambda (c: C).(clear c1 c)) (getl_gen_O c1 c3 H) (CHead
+x1 (Bind x0) x2) H2) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c:
+C).(getl O c c)) (getl_refl x0 x1 x2) c3 H2)))))) H1)) c2 (clear_mono c1 c3
+(getl_gen_O c1 c3 H) c2 H0))))))) (\lambda (n: nat).(\lambda (_: ((\forall
+(c1: C).(\forall (c3: C).((getl n c1 c3) \to (\forall (c2: C).((clear c1 c2)
+\to (getl n c2 c3)))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall
+(c3: C).((getl (S n) c c3) \to (\forall (c2: C).((clear c c2) \to (getl (S n)
+c2 c3)))))) (\lambda (n0: nat).(\lambda (c3: C).(\lambda (H0: (getl (S n)
+(CSort n0) c3)).(\lambda (c2: C).(\lambda (_: (clear (CSort n0)
+c2)).(getl_gen_sort n0 (S n) c3 H0 (getl (S n) c2 c3))))))) (\lambda (c:
+C).(\lambda (H0: ((\forall (c3: C).((getl (S n) c c3) \to (\forall (c2:
+C).((clear c c2) \to (getl (S n) c2 c3))))))).(\lambda (k: K).(\lambda (t:
+T).(\lambda (c3: C).(\lambda (H1: (getl (S n) (CHead c k t) c3)).(\lambda
+(c2: C).(\lambda (H2: (clear (CHead c k t) c2)).(K_ind (\lambda (k0:
+K).((getl (S n) (CHead c k0 t) c3) \to ((clear (CHead c k0 t) c2) \to (getl
+(S n) c2 c3)))) (\lambda (b: B).(\lambda (H3: (getl (S n) (CHead c (Bind b)
+t) c3)).(\lambda (H4: (clear (CHead c (Bind b) t) c2)).(eq_ind_r C (CHead c
+(Bind b) t) (\lambda (c0: C).(getl (S n) c0 c3)) (getl_head (Bind b) n c c3
+(getl_gen_S (Bind b) c c3 t n H3) t) c2 (clear_gen_bind b c c2 t H4)))))
+(\lambda (f: F).(\lambda (H3: (getl (S n) (CHead c (Flat f) t) c3)).(\lambda
+(H4: (clear (CHead c (Flat f) t) c2)).(H0 c3 (getl_gen_S (Flat f) c c3 t n
+H3) c2 (clear_gen_flat f c c2 t H4))))) k H1 H2))))))))) c1)))) i).