- \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e1:
-C).(\forall (v: T).((clear c0 (CHead e1 (Bind b) v)) \to (\forall (e2:
-C).(\forall (n: nat).((getl n e1 e2) \to (getl (S n) c0 e2)))))))) (\lambda
-(n: nat).(\lambda (e1: C).(\lambda (v: T).(\lambda (H: (clear (CSort n)
-(CHead e1 (Bind b) v))).(\lambda (e2: C).(\lambda (n0: nat).(\lambda (_:
-(getl n0 e1 e2)).(clear_gen_sort (CHead e1 (Bind b) v) n H (getl (S n0)
-(CSort n) e2))))))))) (\lambda (c0: C).(\lambda (H: ((\forall (e1:
-C).(\forall (v: T).((clear c0 (CHead e1 (Bind b) v)) \to (\forall (e2:
-C).(\forall (n: nat).((getl n e1 e2) \to (getl (S n) c0 e2))))))))).(\lambda
-(k: K).(\lambda (t: T).(\lambda (e1: C).(\lambda (v: T).(\lambda (H0: (clear
-(CHead c0 k t) (CHead e1 (Bind b) v))).(\lambda (e2: C).(\lambda (n:
-nat).(\lambda (H1: (getl n e1 e2)).(K_ind (\lambda (k0: K).((clear (CHead c0
-k0 t) (CHead e1 (Bind b) v)) \to (getl (S n) (CHead c0 k0 t) e2))) (\lambda
-(b0: B).(\lambda (H2: (clear (CHead c0 (Bind b0) t) (CHead e1 (Bind b)
-v))).(let H3 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
-(_: C).C) with [(CSort _) \Rightarrow e1 | (CHead c1 _ _) \Rightarrow c1]))
-(CHead e1 (Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1
-(Bind b) v) t H2)) in ((let H4 \def (f_equal C B (\lambda (e: C).(match e in
-C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k0 _)
-\Rightarrow (match k0 in K return (\lambda (_: K).B) with [(Bind b1)
-\Rightarrow b1 | (Flat _) \Rightarrow b])])) (CHead e1 (Bind b) v) (CHead c0
-(Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b) v) t H2)) in ((let H5
-\def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
-with [(CSort _) \Rightarrow v | (CHead _ _ t0) \Rightarrow t0])) (CHead e1
-(Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b)
-v) t H2)) in (\lambda (H6: (eq B b b0)).(\lambda (H7: (eq C e1 c0)).(let H8
-\def (eq_ind C e1 (\lambda (c1: C).(getl n c1 e2)) H1 c0 H7) in (eq_ind B b
-(\lambda (b1: B).(getl (S n) (CHead c0 (Bind b1) t) e2)) (getl_head (Bind b)
-n c0 e2 H8 t) b0 H6))))) H4)) H3)))) (\lambda (f: F).(\lambda (H2: (clear
-(CHead c0 (Flat f) t) (CHead e1 (Bind b) v))).(getl_flat c0 e2 (S n) (H e1 v
-(clear_gen_flat f c0 (CHead e1 (Bind b) v) t H2) e2 n H1) f t))) k
-H0))))))))))) c)).
-(* COMMENTS
-Initial nodes: 599
-END *)
+ \lambda (b: B).(\lambda (c: C).(let TMP_2 \def (\lambda (c0: C).(\forall
+(e1: C).(\forall (v: T).((clear c0 (CHead e1 (Bind b) v)) \to (\forall (e2:
+C).(\forall (n: nat).((getl n e1 e2) \to (let TMP_1 \def (S n) in (getl TMP_1
+c0 e2))))))))) in (let TMP_8 \def (\lambda (n: nat).(\lambda (e1: C).(\lambda
+(v: T).(\lambda (H: (clear (CSort n) (CHead e1 (Bind b) v))).(\lambda (e2:
+C).(\lambda (n0: nat).(\lambda (_: (getl n0 e1 e2)).(let TMP_3 \def (Bind b)
+in (let TMP_4 \def (CHead e1 TMP_3 v) in (let TMP_5 \def (S n0) in (let TMP_6
+\def (CSort n) in (let TMP_7 \def (getl TMP_5 TMP_6 e2) in (clear_gen_sort
+TMP_4 n H TMP_7))))))))))))) in (let TMP_52 \def (\lambda (c0: C).(\lambda
+(H: ((\forall (e1: C).(\forall (v: T).((clear c0 (CHead e1 (Bind b) v)) \to
+(\forall (e2: C).(\forall (n: nat).((getl n e1 e2) \to (getl (S n) c0
+e2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e1: C).(\lambda (v:
+T).(\lambda (H0: (clear (CHead c0 k t) (CHead e1 (Bind b) v))).(\lambda (e2:
+C).(\lambda (n: nat).(\lambda (H1: (getl n e1 e2)).(let TMP_11 \def (\lambda
+(k0: K).((clear (CHead c0 k0 t) (CHead e1 (Bind b) v)) \to (let TMP_9 \def (S
+n) in (let TMP_10 \def (CHead c0 k0 t) in (getl TMP_9 TMP_10 e2))))) in (let
+TMP_45 \def (\lambda (b0: B).(\lambda (H2: (clear (CHead c0 (Bind b0) t)
+(CHead e1 (Bind b) v))).(let TMP_12 \def (\lambda (e: C).(match e with
+[(CSort _) \Rightarrow e1 | (CHead c1 _ _) \Rightarrow c1])) in (let TMP_13
+\def (Bind b) in (let TMP_14 \def (CHead e1 TMP_13 v) in (let TMP_15 \def
+(Bind b0) in (let TMP_16 \def (CHead c0 TMP_15 t) in (let TMP_17 \def (Bind
+b) in (let TMP_18 \def (CHead e1 TMP_17 v) in (let TMP_19 \def
+(clear_gen_bind b0 c0 TMP_18 t H2) in (let H3 \def (f_equal C C TMP_12 TMP_14
+TMP_16 TMP_19) in (let TMP_20 \def (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow b | (CHead _ k0 _) \Rightarrow (match k0 with [(Bind b1)
+\Rightarrow b1 | (Flat _) \Rightarrow b])])) in (let TMP_21 \def (Bind b) in
+(let TMP_22 \def (CHead e1 TMP_21 v) in (let TMP_23 \def (Bind b0) in (let
+TMP_24 \def (CHead c0 TMP_23 t) in (let TMP_25 \def (Bind b) in (let TMP_26
+\def (CHead e1 TMP_25 v) in (let TMP_27 \def (clear_gen_bind b0 c0 TMP_26 t
+H2) in (let H4 \def (f_equal C B TMP_20 TMP_22 TMP_24 TMP_27) in (let TMP_28
+\def (\lambda (e: C).(match e with [(CSort _) \Rightarrow v | (CHead _ _ t0)
+\Rightarrow t0])) in (let TMP_29 \def (Bind b) in (let TMP_30 \def (CHead e1
+TMP_29 v) in (let TMP_31 \def (Bind b0) in (let TMP_32 \def (CHead c0 TMP_31
+t) in (let TMP_33 \def (Bind b) in (let TMP_34 \def (CHead e1 TMP_33 v) in
+(let TMP_35 \def (clear_gen_bind b0 c0 TMP_34 t H2) in (let H5 \def (f_equal
+C T TMP_28 TMP_30 TMP_32 TMP_35) in (let TMP_43 \def (\lambda (H6: (eq B b
+b0)).(\lambda (H7: (eq C e1 c0)).(let TMP_36 \def (\lambda (c1: C).(getl n c1
+e2)) in (let H8 \def (eq_ind C e1 TMP_36 H1 c0 H7) in (let TMP_40 \def
+(\lambda (b1: B).(let TMP_37 \def (S n) in (let TMP_38 \def (Bind b1) in (let
+TMP_39 \def (CHead c0 TMP_38 t) in (getl TMP_37 TMP_39 e2))))) in (let TMP_41
+\def (Bind b) in (let TMP_42 \def (getl_head TMP_41 n c0 e2 H8 t) in (eq_ind
+B b TMP_40 TMP_42 b0 H6)))))))) in (let TMP_44 \def (TMP_43 H4) in (TMP_44
+H3)))))))))))))))))))))))))))))))) in (let TMP_51 \def (\lambda (f:
+F).(\lambda (H2: (clear (CHead c0 (Flat f) t) (CHead e1 (Bind b) v))).(let
+TMP_46 \def (S n) in (let TMP_47 \def (Bind b) in (let TMP_48 \def (CHead e1
+TMP_47 v) in (let TMP_49 \def (clear_gen_flat f c0 TMP_48 t H2) in (let
+TMP_50 \def (H e1 v TMP_49 e2 n H1) in (getl_flat c0 e2 TMP_46 TMP_50 f
+t)))))))) in (K_ind TMP_11 TMP_45 TMP_51 k H0)))))))))))))) in (C_ind TMP_2
+TMP_8 TMP_52 c))))).