-ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _)
-\Rightarrow False])) I (S n) H0) in (False_ind P H1))))))) n2)) (\lambda (n:
-nat).(\lambda (H: ((\forall (n2: nat).(or (eq nat n n2) ((eq nat n n2) \to
-(\forall (P: Prop).P)))))).(\lambda (n2: nat).(nat_ind (\lambda (n0: nat).(or
-(eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P: Prop).P)))) (or_intror
-(eq nat (S n) O) ((eq nat (S n) O) \to (\forall (P: Prop).P)) (\lambda (H0:
-(eq nat (S n) O)).(\lambda (P: Prop).(let H1 \def (eq_ind nat (S n) (\lambda
-(ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
-False | (S _) \Rightarrow True])) I O H0) in (False_ind P H1))))) (\lambda
-(n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall
-(P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to (\forall (P:
-Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to (\forall (P:
-Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r nat n0
-(\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P:
-Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq nat (S n) (S
-n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)))) (or_introl (eq nat
-(S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P: Prop).P)) (refl_equal nat
-(S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to (\forall (P:
-Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to
-(\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P:
-Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e in nat return
-(\lambda (_: nat).nat) with [O \Rightarrow n | (S n3) \Rightarrow n3])) (S n)
-(S n0) H2) in (let H4 \def (eq_ind_r nat n0 (\lambda (n3: nat).((eq nat n n3)
-\to (\forall (P0: Prop).P0))) H1 n H3) in (let H5 \def (eq_ind_r nat n0
-(\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0:
-Prop).P0)))) H0 n H3) in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2))))
-n1).
-(* COMMENTS
-Initial nodes: 676
-END *)
+ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I (S n) H0)
+in (False_ind P H1))))))) n2)) (\lambda (n: nat).(\lambda (H: ((\forall (n2:
+nat).(or (eq nat n n2) ((eq nat n n2) \to (\forall (P: Prop).P)))))).(\lambda
+(n2: nat).(nat_ind (\lambda (n0: nat).(or (eq nat (S n) n0) ((eq nat (S n)
+n0) \to (\forall (P: Prop).P)))) (or_intror (eq nat (S n) O) ((eq nat (S n)
+O) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat (S n) O)).(\lambda (P:
+Prop).(let H1 \def (eq_ind nat (S n) (\lambda (ee: nat).(match ee in nat with
+[O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind P
+H1))))) (\lambda (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n)
+n0) \to (\forall (P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to
+(\forall (P: Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to
+(\forall (P: Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r
+nat n0 (\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to
+(\forall (P: Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq
+nat (S n) (S n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P))))
+(or_introl (eq nat (S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P:
+Prop).P)) (refl_equal nat (S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to
+(\forall (P: Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S
+n0)) \to (\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda
+(P: Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e in nat
+with [O \Rightarrow n | (S n3) \Rightarrow n3])) (S n) (S n0) H2) in (let H4
+\def (eq_ind_r nat n0 (\lambda (n3: nat).((eq nat n n3) \to (\forall (P0:
+Prop).P0))) H1 n H3) in (let H5 \def (eq_ind_r nat n0 (\lambda (n3: nat).(or
+(eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0: Prop).P0)))) H0 n H3)
+in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2)))) n1).