-\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 *)
+\def (f_equal C T (\lambda (e: C).(match e 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)).