- \lambda (n: nat).(\lambda (m: nat).(let TMP_204 \def (\lambda (n0:
-nat).(\lambda (n1: nat).(let TMP_203 \def (le n0 n1) in (let TMP_202 \def (lt
-n1 n0) in (or TMP_203 TMP_202))))) in (let TMP_201 \def (\lambda (n0:
-nat).(let TMP_200 \def (le O n0) in (let TMP_199 \def (lt n0 O) in (let
-TMP_198 \def (le_O_n n0) in (or_introl TMP_200 TMP_199 TMP_198))))) in (let
-TMP_197 \def (\lambda (n0: nat).(let TMP_195 \def (S n0) in (let TMP_196 \def
-(le TMP_195 O) in (let TMP_193 \def (S n0) in (let TMP_194 \def (lt O
-TMP_193) in (let TMP_191 \def (S n0) in (let TMP_190 \def (lt_O_Sn n0) in
-(let TMP_192 \def (lt_le_S O TMP_191 TMP_190) in (or_intror TMP_196 TMP_194
-TMP_192))))))))) in (let TMP_189 \def (\lambda (n0: nat).(\lambda (m0:
-nat).(\lambda (H: (or (le n0 m0) (lt m0 n0))).(let TMP_188 \def (le n0 m0) in
-(let TMP_187 \def (lt m0 n0) in (let TMP_184 \def (S n0) in (let TMP_183 \def
-(S m0) in (let TMP_185 \def (le TMP_184 TMP_183) in (let TMP_181 \def (S m0)
-in (let TMP_180 \def (S n0) in (let TMP_182 \def (lt TMP_181 TMP_180) in (let
-TMP_186 \def (or TMP_185 TMP_182) in (let TMP_179 \def (\lambda (H0: (le n0
-m0)).(let TMP_177 \def (S n0) in (let TMP_176 \def (S m0) in (let TMP_178
-\def (le TMP_177 TMP_176) in (let TMP_174 \def (S m0) in (let TMP_173 \def (S
-n0) in (let TMP_175 \def (lt TMP_174 TMP_173) in (let TMP_172 \def (le_n_S n0
-m0 H0) in (or_introl TMP_178 TMP_175 TMP_172))))))))) in (let TMP_171 \def
-(\lambda (H0: (lt m0 n0)).(let TMP_169 \def (S n0) in (let TMP_168 \def (S
-m0) in (let TMP_170 \def (le TMP_169 TMP_168) in (let TMP_166 \def (S m0) in
-(let TMP_165 \def (S n0) in (let TMP_167 \def (lt TMP_166 TMP_165) in (let
-TMP_163 \def (S m0) in (let TMP_164 \def (le_n_S TMP_163 n0 H0) in (or_intror
-TMP_170 TMP_167 TMP_164)))))))))) in (or_ind TMP_188 TMP_187 TMP_186 TMP_179
-TMP_171 H))))))))))))))) in (nat_double_ind TMP_204 TMP_201 TMP_197 TMP_189 n
-m)))))).
+ \lambda (n: nat).(\lambda (m: nat).(let TMP_3 \def (\lambda (n0:
+nat).(\lambda (n1: nat).(let TMP_1 \def (le n0 n1) in (let TMP_2 \def (lt n1
+n0) in (or TMP_1 TMP_2))))) in (let TMP_7 \def (\lambda (n0: nat).(let TMP_4
+\def (le O n0) in (let TMP_5 \def (lt n0 O) in (let TMP_6 \def (le_O_n n0) in
+(or_introl TMP_4 TMP_5 TMP_6))))) in (let TMP_15 \def (\lambda (n0: nat).(let
+TMP_8 \def (S n0) in (let TMP_9 \def (le TMP_8 O) in (let TMP_10 \def (S n0)
+in (let TMP_11 \def (lt O TMP_10) in (let TMP_12 \def (S n0) in (let TMP_13
+\def (lt_O_Sn n0) in (let TMP_14 \def (lt_le_S O TMP_12 TMP_13) in (or_intror
+TMP_9 TMP_11 TMP_14))))))))) in (let TMP_42 \def (\lambda (n0: nat).(\lambda
+(m0: nat).(\lambda (H: (or (le n0 m0) (lt m0 n0))).(let TMP_16 \def (le n0
+m0) in (let TMP_17 \def (lt m0 n0) in (let TMP_18 \def (S n0) in (let TMP_19
+\def (S m0) in (let TMP_20 \def (le TMP_18 TMP_19) in (let TMP_21 \def (S m0)
+in (let TMP_22 \def (S n0) in (let TMP_23 \def (lt TMP_21 TMP_22) in (let
+TMP_24 \def (or TMP_20 TMP_23) in (let TMP_32 \def (\lambda (H0: (le n0
+m0)).(let TMP_25 \def (S n0) in (let TMP_26 \def (S m0) in (let TMP_27 \def
+(le TMP_25 TMP_26) in (let TMP_28 \def (S m0) in (let TMP_29 \def (S n0) in
+(let TMP_30 \def (lt TMP_28 TMP_29) in (let TMP_31 \def (le_n_S n0 m0 H0) in
+(or_introl TMP_27 TMP_30 TMP_31))))))))) in (let TMP_41 \def (\lambda (H0:
+(lt m0 n0)).(let TMP_33 \def (S n0) in (let TMP_34 \def (S m0) in (let TMP_35
+\def (le TMP_33 TMP_34) in (let TMP_36 \def (S m0) in (let TMP_37 \def (S n0)
+in (let TMP_38 \def (lt TMP_36 TMP_37) in (let TMP_39 \def (S m0) in (let
+TMP_40 \def (le_n_S TMP_39 n0 H0) in (or_intror TMP_35 TMP_38
+TMP_40)))))))))) in (or_ind TMP_16 TMP_17 TMP_24 TMP_32 TMP_41
+H))))))))))))))) in (nat_double_ind TMP_3 TMP_7 TMP_15 TMP_42 n m)))))).