-(e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d0
-| (CHead c2 _ _) \Rightarrow c2])) (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind
-b) t1) (clear_gen_bind b c0 (CHead d0 (Bind Abbr) u0) t1 H12)) in ((let H14
-\def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B)
-with [(CSort _) \Rightarrow Abbr | (CHead _ k0 _) \Rightarrow (match k0 in K
-return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
-\Rightarrow Abbr])])) (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t1)
-(clear_gen_bind b c0 (CHead d0 (Bind Abbr) u0) t1 H12)) in ((let H15 \def
-(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
-[(CSort _) \Rightarrow u0 | (CHead _ _ t7) \Rightarrow t7])) (CHead d0 (Bind
-Abbr) u0) (CHead c0 (Bind b) t1) (clear_gen_bind b c0 (CHead d0 (Bind Abbr)
-u0) t1 H12)) in (\lambda (H16: (eq B Abbr b)).(\lambda (_: (eq C d0 c0)).(let
-H18 \def (eq_ind T u0 (\lambda (t7: T).(subst0 O t7 t5 t6)) H11 t1 H15) in
-(eq_ind B Abbr (\lambda (b0: B).(pc3 (CHead c0 (Bind b0) t) t4 t6)) (ex2_ind
-T (\lambda (t7: T).(subst0 O t2 t5 t7)) (\lambda (t7: T).(pr0 t6 t7)) (pc3
-(CHead c0 (Bind Abbr) t) t4 t6) (\lambda (x: T).(\lambda (H19: (subst0 O t2
-t5 x)).(\lambda (H20: (pr0 t6 x)).(ex2_ind T (\lambda (t7: T).(subst0 O t t5
-t7)) (\lambda (t7: T).(subst0 (S (plus i O)) u x t7)) (pc3 (CHead c0 (Bind
-Abbr) t) t4 t6) (\lambda (x0: T).(\lambda (H21: (subst0 O t t5 x0)).(\lambda
-(H22: (subst0 (S (plus i O)) u x x0)).(let H23 \def (f_equal nat nat S (plus
-i O) i (sym_eq nat i (plus i O) (plus_n_O i))) in (let H24 \def (eq_ind nat
-(S (plus i O)) (\lambda (n: nat).(subst0 n u x x0)) H22 (S i) H23) in
-(pc3_pr2_u (CHead c0 (Bind Abbr) t) x0 t4 (pr2_delta (CHead c0 (Bind Abbr) t)
-c0 t O (getl_refl Abbr c0 t) t4 t5 H6 x0 H21) t6 (pc3_pr2_x (CHead c0 (Bind
-Abbr) t) x0 t6 (pr2_delta (CHead c0 (Bind Abbr) t) d u (S i) (getl_head (Bind
-Abbr) i c0 (CHead d (Bind Abbr) u) H0 t) t6 x H20 x0 H24))))))))
-(subst0_subst0_back t5 x t2 O H19 t u i H2))))) (pr0_subst0_fwd t1 t5 t6 O
-H18 t2 H1)) b H16))))) H14)) H13)))) (\lambda (f: F).(\lambda (H12: (clear
-(CHead c0 (Flat f) t1) (CHead d0 (Bind Abbr) u0))).(clear_pc3_trans (CHead d0
-(Bind Abbr) u0) t4 t6 (pc3_pr2_r (CHead d0 (Bind Abbr) u0) t4 t6 (pr2_delta
-(CHead d0 (Bind Abbr) u0) d0 u0 O (getl_refl Abbr d0 u0) t4 t5 H6 t6 H11))
-(CHead c0 (Flat f) t) (clear_flat c0 (CHead d0 (Bind Abbr) u0)
-(clear_gen_flat f c0 (CHead d0 (Bind Abbr) u0) t1 H12) f t)))) k (getl_gen_O
-(CHead c0 k t1) (CHead d0 (Bind Abbr) u0) H10)))) (\lambda (i1: nat).(\lambda
-(_: (((getl i1 (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)) \to ((subst0 i1 u0
-t5 t6) \to (pc3 (CHead c0 k t) t4 t6))))).(\lambda (H10: (getl (S i1) (CHead
-c0 k t1) (CHead d0 (Bind Abbr) u0))).(\lambda (H11: (subst0 (S i1) u0 t5
-t6)).(K_ind (\lambda (k0: K).((getl (r k0 i1) c0 (CHead d0 (Bind Abbr) u0))
-\to (pc3 (CHead c0 k0 t) t4 t6))) (\lambda (b: B).(\lambda (H12: (getl (r
-(Bind b) i1) c0 (CHead d0 (Bind Abbr) u0))).(pc3_pr2_r (CHead c0 (Bind b) t)
-t4 t6 (pr2_delta (CHead c0 (Bind b) t) d0 u0 (S i1) (getl_head (Bind b) i1 c0
-(CHead d0 (Bind Abbr) u0) H12 t) t4 t5 H6 t6 H11)))) (\lambda (f: F).(\lambda
-(H12: (getl (r (Flat f) i1) c0 (CHead d0 (Bind Abbr) u0))).(pc3_pr2_r (CHead
-c0 (Flat f) t) t4 t6 (pr2_cflat c0 t4 t6 (pr2_delta c0 d0 u0 (r (Flat f) i1)
-H12 t4 t5 H6 t6 H11) f t)))) k (getl_gen_S k c0 (CHead d0 (Bind Abbr) u0) t1
-i1 H10)))))) i0 H9 H7))))))))))))) y t0 t3 H4))) H3))))))))))))))) c u2 u1
-H)))).
-(* COMMENTS
-Initial nodes: 1671
-END *)
+(e: C).(match e with [(CSort _) \Rightarrow d0 | (CHead c2 _ _) \Rightarrow
+c2])) (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t1) (clear_gen_bind b c0
+(CHead d0 (Bind Abbr) u0) t1 H12)) in ((let H14 \def (f_equal C B (\lambda
+(e: C).(match e with [(CSort _) \Rightarrow Abbr | (CHead _ k0 _) \Rightarrow
+(match k0 with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abbr])]))
+(CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t1) (clear_gen_bind b c0 (CHead
+d0 (Bind Abbr) u0) t1 H12)) in ((let H15 \def (f_equal C T (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow u0 | (CHead _ _ t7) \Rightarrow t7]))
+(CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t1) (clear_gen_bind b c0 (CHead
+d0 (Bind Abbr) u0) t1 H12)) in (\lambda (H16: (eq B Abbr b)).(\lambda (_: (eq
+C d0 c0)).(let H18 \def (eq_ind T u0 (\lambda (t7: T).(subst0 O t7 t5 t6))
+H11 t1 H15) in (eq_ind B Abbr (\lambda (b0: B).(pc3 (CHead c0 (Bind b0) t) t4
+t6)) (ex2_ind T (\lambda (t7: T).(subst0 O t2 t5 t7)) (\lambda (t7: T).(pr0
+t6 t7)) (pc3 (CHead c0 (Bind Abbr) t) t4 t6) (\lambda (x: T).(\lambda (H19:
+(subst0 O t2 t5 x)).(\lambda (H20: (pr0 t6 x)).(ex2_ind T (\lambda (t7:
+T).(subst0 O t t5 t7)) (\lambda (t7: T).(subst0 (S (plus i O)) u x t7)) (pc3
+(CHead c0 (Bind Abbr) t) t4 t6) (\lambda (x0: T).(\lambda (H21: (subst0 O t
+t5 x0)).(\lambda (H22: (subst0 (S (plus i O)) u x x0)).(let H23 \def (f_equal
+nat nat S (plus i O) i (sym_eq nat i (plus i O) (plus_n_O i))) in (let H24
+\def (eq_ind nat (S (plus i O)) (\lambda (n: nat).(subst0 n u x x0)) H22 (S
+i) H23) in (pc3_pr2_u (CHead c0 (Bind Abbr) t) x0 t4 (pr2_delta (CHead c0
+(Bind Abbr) t) c0 t O (getl_refl Abbr c0 t) t4 t5 H6 x0 H21) t6 (pc3_pr2_x
+(CHead c0 (Bind Abbr) t) x0 t6 (pr2_delta (CHead c0 (Bind Abbr) t) d u (S i)
+(getl_head (Bind Abbr) i c0 (CHead d (Bind Abbr) u) H0 t) t6 x H20 x0
+H24)))))))) (subst0_subst0_back t5 x t2 O H19 t u i H2))))) (pr0_subst0_fwd
+t1 t5 t6 O H18 t2 H1)) b H16))))) H14)) H13)))) (\lambda (f: F).(\lambda
+(H12: (clear (CHead c0 (Flat f) t1) (CHead d0 (Bind Abbr)
+u0))).(clear_pc3_trans (CHead d0 (Bind Abbr) u0) t4 t6 (pc3_pr2_r (CHead d0
+(Bind Abbr) u0) t4 t6 (pr2_delta (CHead d0 (Bind Abbr) u0) d0 u0 O (getl_refl
+Abbr d0 u0) t4 t5 H6 t6 H11)) (CHead c0 (Flat f) t) (clear_flat c0 (CHead d0
+(Bind Abbr) u0) (clear_gen_flat f c0 (CHead d0 (Bind Abbr) u0) t1 H12) f
+t)))) k (getl_gen_O (CHead c0 k t1) (CHead d0 (Bind Abbr) u0) H10))))
+(\lambda (i1: nat).(\lambda (_: (((getl i1 (CHead c0 k t1) (CHead d0 (Bind
+Abbr) u0)) \to ((subst0 i1 u0 t5 t6) \to (pc3 (CHead c0 k t) t4
+t6))))).(\lambda (H10: (getl (S i1) (CHead c0 k t1) (CHead d0 (Bind Abbr)
+u0))).(\lambda (H11: (subst0 (S i1) u0 t5 t6)).(K_ind (\lambda (k0: K).((getl
+(r k0 i1) c0 (CHead d0 (Bind Abbr) u0)) \to (pc3 (CHead c0 k0 t) t4 t6)))
+(\lambda (b: B).(\lambda (H12: (getl (r (Bind b) i1) c0 (CHead d0 (Bind Abbr)
+u0))).(pc3_pr2_r (CHead c0 (Bind b) t) t4 t6 (pr2_delta (CHead c0 (Bind b) t)
+d0 u0 (S i1) (getl_head (Bind b) i1 c0 (CHead d0 (Bind Abbr) u0) H12 t) t4 t5
+H6 t6 H11)))) (\lambda (f: F).(\lambda (H12: (getl (r (Flat f) i1) c0 (CHead
+d0 (Bind Abbr) u0))).(pc3_pr2_r (CHead c0 (Flat f) t) t4 t6 (pr2_cflat c0 t4
+t6 (pr2_delta c0 d0 u0 (r (Flat f) i1) H12 t4 t5 H6 t6 H11) f t)))) k
+(getl_gen_S k c0 (CHead d0 (Bind Abbr) u0) t1 i1 H10)))))) i0 H9
+H7))))))))))))) y t0 t3 H4))) H3))))))))))))))) c u2 u1 H)))).