-e2)).(let H1 \def (getl_gen_all c2 e2 i H0) in (ex2_ind C (\lambda (e:
-C).(drop i O c2 e)) (\lambda (e: C).(clear e e2)) (getl (plus i h) c1 e2)
-(\lambda (x: C).(\lambda (H2: (drop i O c2 x)).(\lambda (H3: (clear x
-e2)).(nat_ind (\lambda (n: nat).((drop n O c2 x) \to (getl (plus n h) c1
-e2))) (\lambda (H4: (drop O O c2 x)).(let H5 \def (eq_ind_r C x (\lambda (c:
-C).(clear c e2)) H3 c2 (drop_gen_refl c2 x H4)) in (getl_clear_trans (plus O
-h) c1 c2 H e2 H5))) (\lambda (i0: nat).(\lambda (_: (((drop i0 O c2 x) \to
-(getl (plus i0 h) c1 e2)))).(\lambda (H4: (drop (S i0) O c2 x)).(let H_y \def
-(getl_drop_trans c1 c2 h H x i0 H4) in (getl_intro (plus (S i0) h) c1 e2 x
-H_y H3))))) i H2)))) H1)))))))).
-(* COMMENTS
-Initial nodes: 247
-END *)
+e2)).(let H1 \def (getl_gen_all c2 e2 i H0) in (let TMP_1 \def (\lambda (e:
+C).(drop i O c2 e)) in (let TMP_2 \def (\lambda (e: C).(clear e e2)) in (let
+TMP_3 \def (plus i h) in (let TMP_4 \def (getl TMP_3 c1 e2) in (let TMP_14
+\def (\lambda (x: C).(\lambda (H2: (drop i O c2 x)).(\lambda (H3: (clear x
+e2)).(let TMP_6 \def (\lambda (n: nat).((drop n O c2 x) \to (let TMP_5 \def
+(plus n h) in (getl TMP_5 c1 e2)))) in (let TMP_10 \def (\lambda (H4: (drop O
+O c2 x)).(let TMP_7 \def (\lambda (c: C).(clear c e2)) in (let TMP_8 \def
+(drop_gen_refl c2 x H4) in (let H5 \def (eq_ind_r C x TMP_7 H3 c2 TMP_8) in
+(let TMP_9 \def (plus O h) in (getl_clear_trans TMP_9 c1 c2 H e2 H5)))))) in
+(let TMP_13 \def (\lambda (i0: nat).(\lambda (_: (((drop i0 O c2 x) \to (getl
+(plus i0 h) c1 e2)))).(\lambda (H4: (drop (S i0) O c2 x)).(let H_y \def
+(getl_drop_trans c1 c2 h H x i0 H4) in (let TMP_11 \def (S i0) in (let TMP_12
+\def (plus TMP_11 h) in (getl_intro TMP_12 c1 e2 x H_y H3))))))) in (nat_ind
+TMP_6 TMP_10 TMP_13 i H2))))))) in (ex2_ind C TMP_1 TMP_2 TMP_4 TMP_14
+H1))))))))))))).