- \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq nat (plus n y) O) \to (land (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda (H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O) \to (land (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq nat (plus (S n) y) O)).(let H1 \def (match H0 return (\lambda (n0: nat).((eq nat n0 O) \to (land (eq nat (S n) O) (eq nat y O)))) with [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n) y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq nat (plus n y) O) \to (land (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda (H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O) \to (land (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq nat (plus (S n) y) O)).(let H1 \def (match H0 return (\lambda (n0: nat).(\lambda (_: (eq ? ? n0)).((eq nat n0 O) \to (land (eq nat (S n) O) (eq nat y O))))) with [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n) y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y O)) H2)))]) in (H1 (refl_equal nat O))))))) x).