-in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d1 | (CHead c _ _)
-\Rightarrow c])) (CHead d1 (Bind b0) w) (CHead c1 (Bind b) v) (clear_gen_bind
-b c1 (CHead d1 (Bind b0) w) v (getl_gen_O (CHead c1 (Bind b) v) (CHead d1
-(Bind b0) w) H1))) in ((let H3 \def (f_equal C B (\lambda (e: C).(match e in
-C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b0 | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b1)
-\Rightarrow b1 | (Flat _) \Rightarrow b0])])) (CHead d1 (Bind b0) w) (CHead
-c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1 (Bind b0) w) v (getl_gen_O
-(CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1))) in ((let H4 \def (f_equal
-C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
-\Rightarrow w | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b0) w) (CHead
-c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1 (Bind b0) w) v (getl_gen_O
-(CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1))) in (\lambda (H5: (eq B b0
-b)).(\lambda (_: (eq C d1 c1)).(eq_ind_r T v (\lambda (t: T).(ex C (\lambda
-(d2: C).(getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b0) t))))) (eq_ind_r B
-b (\lambda (b1: B).(ex C (\lambda (d2: C).(getl O (CHead c2 (Bind b) v)
-(CHead d2 (Bind b1) v))))) (ex_intro C (\lambda (d2: C).(getl O (CHead c2
-(Bind b) v) (CHead d2 (Bind b) v))) c2 (getl_refl b c2 v)) b0 H5) w H4))))
-H3)) H2))) (\lambda (h0: nat).(\lambda (_: (((getl h0 (CHead c1 (Bind b) v)
-(CHead d1 (Bind b0) w)) \to (ex C (\lambda (d2: C).(getl h0 (CHead c2 (Bind
-b) v) (CHead d2 (Bind b0) w))))))).(\lambda (H1: (getl (S h0) (CHead c1 (Bind
-b) v) (CHead d1 (Bind b0) w))).(let H_x \def (H b0 d1 w (r (Bind b) h0)
-(getl_gen_S (Bind b) c1 (CHead d1 (Bind b0) w) v h0 H1)) in (let H2 \def H_x
-in (ex_ind C (\lambda (d2: C).(getl h0 c2 (CHead d2 (Bind b0) w))) (ex C
-(\lambda (d2: C).(getl (S h0) (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w))))
-(\lambda (x: C).(\lambda (H3: (getl h0 c2 (CHead x (Bind b0) w))).(ex_intro C
-(\lambda (d2: C).(getl (S h0) (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)))
-x (getl_head (Bind b) h0 c2 (CHead x (Bind b0) w) H3 v)))) H2)))))) h
-H0)))))))))).
-(* COMMENTS
-Initial nodes: 817
-END *)
+with [(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1
+(Bind b0) w) (CHead c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1 (Bind b0)
+w) v (getl_gen_O (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1))) in ((let
+H3 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow b0
+| (CHead _ k _) \Rightarrow (match k with [(Bind b1) \Rightarrow b1 | (Flat
+_) \Rightarrow b0])])) (CHead d1 (Bind b0) w) (CHead c1 (Bind b) v)
+(clear_gen_bind b c1 (CHead d1 (Bind b0) w) v (getl_gen_O (CHead c1 (Bind b)
+v) (CHead d1 (Bind b0) w) H1))) in ((let H4 \def (f_equal C T (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow w | (CHead _ _ t) \Rightarrow t]))
+(CHead d1 (Bind b0) w) (CHead c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1
+(Bind b0) w) v (getl_gen_O (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1)))
+in (\lambda (H5: (eq B b0 b)).(\lambda (_: (eq C d1 c1)).(eq_ind_r T v
+(\lambda (t: T).(ex C (\lambda (d2: C).(getl O (CHead c2 (Bind b) v) (CHead
+d2 (Bind b0) t))))) (eq_ind_r B b (\lambda (b1: B).(ex C (\lambda (d2:
+C).(getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b1) v))))) (ex_intro C
+(\lambda (d2: C).(getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b) v))) c2
+(getl_refl b c2 v)) b0 H5) w H4)))) H3)) H2))) (\lambda (h0: nat).(\lambda
+(_: (((getl h0 (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)) \to (ex C
+(\lambda (d2: C).(getl h0 (CHead c2 (Bind b) v) (CHead d2 (Bind b0)
+w))))))).(\lambda (H1: (getl (S h0) (CHead c1 (Bind b) v) (CHead d1 (Bind b0)
+w))).(let H_x \def (H b0 d1 w (r (Bind b) h0) (getl_gen_S (Bind b) c1 (CHead
+d1 (Bind b0) w) v h0 H1)) in (let H2 \def H_x in (ex_ind C (\lambda (d2:
+C).(getl h0 c2 (CHead d2 (Bind b0) w))) (ex C (\lambda (d2: C).(getl (S h0)
+(CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)))) (\lambda (x: C).(\lambda (H3:
+(getl h0 c2 (CHead x (Bind b0) w))).(ex_intro C (\lambda (d2: C).(getl (S h0)
+(CHead c2 (Bind b) v) (CHead d2 (Bind b0) w))) x (getl_head (Bind b) h0 c2
+(CHead x (Bind b0) w) H3 v)))) H2)))))) h H0)))))))))).