- \lambda (n1: nat).(let TMP_81 \def (\lambda (n: nat).(\forall (n2: nat).(let
-TMP_80 \def (eq nat n n2) in (let TMP_79 \def ((eq nat n n2) \to (\forall (P:
-Prop).P)) in (or TMP_80 TMP_79))))) in (let TMP_78 \def (\lambda (n2:
-nat).(let TMP_77 \def (\lambda (n: nat).(let TMP_76 \def (eq nat O n) in (let
-TMP_75 \def ((eq nat O n) \to (\forall (P: Prop).P)) in (or TMP_76 TMP_75))))
-in (let TMP_73 \def (eq nat O O) in (let TMP_72 \def ((eq nat O O) \to
-(\forall (P: Prop).P)) in (let TMP_71 \def (refl_equal nat O) in (let TMP_74
-\def (or_introl TMP_73 TMP_72 TMP_71) in (let TMP_70 \def (\lambda (n:
-nat).(\lambda (_: (or (eq nat O n) ((eq nat O n) \to (\forall (P:
-Prop).P)))).(let TMP_68 \def (S n) in (let TMP_69 \def (eq nat O TMP_68) in
-(let TMP_67 \def ((eq nat O (S n)) \to (\forall (P: Prop).P)) in (let TMP_66
-\def (\lambda (H0: (eq nat O (S n))).(\lambda (P: Prop).(let TMP_65 \def
-(\lambda (ee: nat).(match ee in nat with [O \Rightarrow True | (S _)
-\Rightarrow False])) in (let TMP_64 \def (S n) in (let H1 \def (eq_ind nat O
-TMP_65 I TMP_64 H0) in (False_ind P H1)))))) in (or_intror TMP_69 TMP_67
-TMP_66))))))) in (nat_ind TMP_77 TMP_74 TMP_70 n2)))))))) in (let TMP_63 \def
-(\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).(let TMP_62 \def
-(\lambda (n0: nat).(let TMP_60 \def (S n) in (let TMP_61 \def (eq nat TMP_60
-n0) in (let TMP_59 \def ((eq nat (S n) n0) \to (\forall (P: Prop).P)) in (or
-TMP_61 TMP_59))))) in (let TMP_56 \def (S n) in (let TMP_57 \def (eq nat
-TMP_56 O) in (let TMP_55 \def ((eq nat (S n) O) \to (\forall (P: Prop).P)) in
-(let TMP_54 \def (\lambda (H0: (eq nat (S n) O)).(\lambda (P: Prop).(let
-TMP_53 \def (S n) in (let TMP_52 \def (\lambda (ee: nat).(match ee in nat
-with [O \Rightarrow False | (S _) \Rightarrow True])) in (let H1 \def (eq_ind
-nat TMP_53 TMP_52 I O H0) in (False_ind P H1)))))) in (let TMP_58 \def
-(or_intror TMP_57 TMP_55 TMP_54) in (let TMP_51 \def (\lambda (n0:
-nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P:
-Prop).P)))).(let TMP_50 \def (eq nat n n0) in (let TMP_49 \def ((eq nat n n0)
-\to (\forall (P: Prop).P)) in (let TMP_46 \def (S n) in (let TMP_45 \def (S
-n0) in (let TMP_47 \def (eq nat TMP_46 TMP_45) in (let TMP_44 \def ((eq nat
-(S n) (S n0)) \to (\forall (P: Prop).P)) in (let TMP_48 \def (or TMP_47
-TMP_44) in (let TMP_43 \def (\lambda (H1: (eq nat n n0)).(let TMP_30 \def
-(\lambda (n3: nat).(let TMP_28 \def (S n) in (let TMP_29 \def (eq nat TMP_28
-n3) in (let TMP_27 \def ((eq nat (S n) n3) \to (\forall (P: Prop).P)) in (or
-TMP_29 TMP_27))))) in (let H2 \def (eq_ind_r nat n0 TMP_30 H0 n H1) in (let
-TMP_42 \def (\lambda (n3: nat).(let TMP_40 \def (S n) in (let TMP_39 \def (S
-n3) in (let TMP_41 \def (eq nat TMP_40 TMP_39) in (let TMP_38 \def ((eq nat
-(S n) (S n3)) \to (\forall (P: Prop).P)) in (or TMP_41 TMP_38)))))) in (let
-TMP_35 \def (S n) in (let TMP_34 \def (S n) in (let TMP_36 \def (eq nat
-TMP_35 TMP_34) in (let TMP_33 \def ((eq nat (S n) (S n)) \to (\forall (P:
-Prop).P)) in (let TMP_31 \def (S n) in (let TMP_32 \def (refl_equal nat
-TMP_31) in (let TMP_37 \def (or_introl TMP_36 TMP_33 TMP_32) in (eq_ind nat n
-TMP_42 TMP_37 n0 H1)))))))))))) in (let TMP_26 \def (\lambda (H1: (((eq nat n
-n0) \to (\forall (P: Prop).P)))).(let TMP_24 \def (S n) in (let TMP_23 \def
-(S n0) in (let TMP_25 \def (eq nat TMP_24 TMP_23) in (let TMP_22 \def ((eq
-nat (S n) (S n0)) \to (\forall (P: Prop).P)) in (let TMP_21 \def (\lambda
-(H2: (eq nat (S n) (S n0))).(\lambda (P: Prop).(let TMP_14 \def (\lambda (e:
-nat).(match e in nat with [O \Rightarrow n | (S n3) \Rightarrow n3])) in (let
-TMP_13 \def (S n) in (let TMP_12 \def (S n0) in (let H3 \def (f_equal nat nat
-TMP_14 TMP_13 TMP_12 H2) in (let TMP_15 \def (\lambda (n3: nat).((eq nat n
-n3) \to (\forall (P0: Prop).P0))) in (let H4 \def (eq_ind_r nat n0 TMP_15 H1
-n H3) in (let TMP_19 \def (\lambda (n3: nat).(let TMP_17 \def (S n) in (let
-TMP_18 \def (eq nat TMP_17 n3) in (let TMP_16 \def ((eq nat (S n) n3) \to
-(\forall (P0: Prop).P0)) in (or TMP_18 TMP_16))))) in (let H5 \def (eq_ind_r
-nat n0 TMP_19 H0 n H3) in (let TMP_20 \def (refl_equal nat n) in (H4 TMP_20
-P)))))))))))) in (or_intror TMP_25 TMP_22 TMP_21))))))) in (let TMP_11 \def
-(H n0) in (or_ind TMP_50 TMP_49 TMP_48 TMP_43 TMP_26 TMP_11))))))))))))) in
-(nat_ind TMP_62 TMP_58 TMP_51 n2))))))))))) in (nat_ind TMP_81 TMP_78 TMP_63
-n1)))).
+ \lambda (n1: nat).(let TMP_3 \def (\lambda (n: nat).(\forall (n2: nat).(let
+TMP_1 \def (eq nat n n2) in (let TMP_2 \def ((eq nat n n2) \to (\forall (P:
+Prop).P)) in (or TMP_1 TMP_2))))) in (let TMP_18 \def (\lambda (n2: nat).(let
+TMP_6 \def (\lambda (n: nat).(let TMP_4 \def (eq nat O n) in (let TMP_5 \def
+((eq nat O n) \to (\forall (P: Prop).P)) in (or TMP_4 TMP_5)))) in (let TMP_7
+\def (eq nat O O) in (let TMP_8 \def ((eq nat O O) \to (\forall (P: Prop).P))
+in (let TMP_9 \def (refl_equal nat O) in (let TMP_10 \def (or_introl TMP_7
+TMP_8 TMP_9) in (let TMP_17 \def (\lambda (n: nat).(\lambda (_: (or (eq nat O
+n) ((eq nat O n) \to (\forall (P: Prop).P)))).(let TMP_11 \def (S n) in (let
+TMP_12 \def (eq nat O TMP_11) in (let TMP_13 \def ((eq nat O (S n)) \to
+(\forall (P: Prop).P)) in (let TMP_16 \def (\lambda (H0: (eq nat O (S
+n))).(\lambda (P: Prop).(let TMP_14 \def (\lambda (ee: nat).(match ee with [O
+\Rightarrow True | (S _) \Rightarrow False])) in (let TMP_15 \def (S n) in
+(let H1 \def (eq_ind nat O TMP_14 I TMP_15 H0) in (False_ind P H1)))))) in
+(or_intror TMP_12 TMP_13 TMP_16))))))) in (nat_ind TMP_6 TMP_10 TMP_17
+n2)))))))) in (let TMP_71 \def (\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).(let TMP_22 \def (\lambda (n0: nat).(let TMP_19 \def (S n) in (let
+TMP_20 \def (eq nat TMP_19 n0) in (let TMP_21 \def ((eq nat (S n) n0) \to
+(\forall (P: Prop).P)) in (or TMP_20 TMP_21))))) in (let TMP_23 \def (S n) in
+(let TMP_24 \def (eq nat TMP_23 O) in (let TMP_25 \def ((eq nat (S n) O) \to
+(\forall (P: Prop).P)) in (let TMP_28 \def (\lambda (H0: (eq nat (S n)
+O)).(\lambda (P: Prop).(let TMP_26 \def (S n) in (let TMP_27 \def (\lambda
+(ee: nat).(match ee with [O \Rightarrow False | (S _) \Rightarrow True])) in
+(let H1 \def (eq_ind nat TMP_26 TMP_27 I O H0) in (False_ind P H1)))))) in
+(let TMP_29 \def (or_intror TMP_24 TMP_25 TMP_28) in (let TMP_70 \def
+(\lambda (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to
+(\forall (P: Prop).P)))).(let TMP_30 \def (eq nat n n0) in (let TMP_31 \def
+((eq nat n n0) \to (\forall (P: Prop).P)) in (let TMP_32 \def (S n) in (let
+TMP_33 \def (S n0) in (let TMP_34 \def (eq nat TMP_32 TMP_33) in (let TMP_35
+\def ((eq nat (S n) (S n0)) \to (\forall (P: Prop).P)) in (let TMP_36 \def
+(or TMP_34 TMP_35) in (let TMP_53 \def (\lambda (H1: (eq nat n n0)).(let
+TMP_40 \def (\lambda (n3: nat).(let TMP_37 \def (S n) in (let TMP_38 \def (eq
+nat TMP_37 n3) in (let TMP_39 \def ((eq nat (S n) n3) \to (\forall (P:
+Prop).P)) in (or TMP_38 TMP_39))))) in (let H2 \def (eq_ind_r nat n0 TMP_40
+H0 n H1) in (let TMP_45 \def (\lambda (n3: nat).(let TMP_41 \def (S n) in
+(let TMP_42 \def (S n3) in (let TMP_43 \def (eq nat TMP_41 TMP_42) in (let
+TMP_44 \def ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)) in (or TMP_43
+TMP_44)))))) in (let TMP_46 \def (S n) in (let TMP_47 \def (S n) in (let
+TMP_48 \def (eq nat TMP_46 TMP_47) in (let TMP_49 \def ((eq nat (S n) (S n))
+\to (\forall (P: Prop).P)) in (let TMP_50 \def (S n) in (let TMP_51 \def
+(refl_equal nat TMP_50) in (let TMP_52 \def (or_introl TMP_48 TMP_49 TMP_51)
+in (eq_ind nat n TMP_45 TMP_52 n0 H1)))))))))))) in (let TMP_68 \def (\lambda
+(H1: (((eq nat n n0) \to (\forall (P: Prop).P)))).(let TMP_54 \def (S n) in
+(let TMP_55 \def (S n0) in (let TMP_56 \def (eq nat TMP_54 TMP_55) in (let
+TMP_57 \def ((eq nat (S n) (S n0)) \to (\forall (P: Prop).P)) in (let TMP_67
+\def (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P: Prop).(let TMP_58 \def
+(\lambda (e: nat).(match e with [O \Rightarrow n | (S n3) \Rightarrow n3]))
+in (let TMP_59 \def (S n) in (let TMP_60 \def (S n0) in (let H3 \def (f_equal
+nat nat TMP_58 TMP_59 TMP_60 H2) in (let TMP_61 \def (\lambda (n3: nat).((eq
+nat n n3) \to (\forall (P0: Prop).P0))) in (let H4 \def (eq_ind_r nat n0
+TMP_61 H1 n H3) in (let TMP_65 \def (\lambda (n3: nat).(let TMP_62 \def (S n)
+in (let TMP_63 \def (eq nat TMP_62 n3) in (let TMP_64 \def ((eq nat (S n) n3)
+\to (\forall (P0: Prop).P0)) in (or TMP_63 TMP_64))))) in (let H5 \def
+(eq_ind_r nat n0 TMP_65 H0 n H3) in (let TMP_66 \def (refl_equal nat n) in
+(H4 TMP_66 P)))))))))))) in (or_intror TMP_56 TMP_57 TMP_67))))))) in (let
+TMP_69 \def (H n0) in (or_ind TMP_30 TMP_31 TMP_36 TMP_53 TMP_68
+TMP_69))))))))))))) in (nat_ind TMP_22 TMP_29 TMP_70 n2))))))))))) in
+(nat_ind TMP_3 TMP_18 TMP_71 n1)))).