-nat (plus n y3) (plus n y4)) \to (eq nat y4 y3))))))) H_y z0 (minus_n_O z0))
-in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (eq_add_S (plus z0 y1) (plus z0 y2)
-H1))))))))) (\lambda (x3: nat).(\lambda (_: ((\forall (y1: nat).(\forall (y2:
-nat).((le O (S z0)) \to ((le x3 (S z0)) \to ((eq nat (S (plus z0 y1)) (plus
-(match x3 with [O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)]) y2))
-\to (eq nat y2 (plus x3 y1))))))))).(\lambda (y1: nat).(\lambda (y2:
-nat).(\lambda (_: (le O (S z0))).(\lambda (H0: (le (S x3) (S z0))).(\lambda
-(H1: (eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2))).(let H_y \def (IH O
-x3 (S y1)) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n:
-nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (plus n (S
-y1)) (plus (minus z0 x3) y3)) \to (eq nat y3 (plus x3 (S y1)))))))) H_y z0
-(minus_n_O z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y1)) (\lambda (n:
-nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat n (plus
-(minus z0 x3) y3)) \to (eq nat y3 (plus x3 (S y1)))))))) H2 (S (plus z0 y1))
-(plus_n_Sm z0 y1)) in (let H4 \def (eq_ind_r nat (plus x3 (S y1)) (\lambda
-(n: nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (S (plus
-z0 y1)) (plus (minus z0 x3) y3)) \to (eq nat y3 n)))))) H3 (S (plus x3 y1))
-(plus_n_Sm x3 y1)) in (H4 y2 (le_O_n z0) (le_S_n x3 z0 H0) H1))))))))))))
-x2)) (\lambda (x2: nat).(\lambda (_: ((\forall (x3: nat).(\forall (y1:
-nat).(\forall (y2: nat).((le x2 (S z0)) \to ((le x3 (S z0)) \to ((eq nat
-(plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2)) \to (eq nat (plus x2
-y2) (plus x3 y1)))))))))).(\lambda (x3: nat).(nat_ind (\lambda (n:
-nat).(\forall (y1: nat).(\forall (y2: nat).((le (S x2) (S z0)) \to ((le n (S
-z0)) \to ((eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2))
-\to (eq nat (plus (S x2) y2) (plus n y1)))))))) (\lambda (y1: nat).(\lambda
-(y2: nat).(\lambda (H: (le (S x2) (S z0))).(\lambda (_: (le O (S
-z0))).(\lambda (H1: (eq nat (plus (minus z0 x2) y1) (S (plus z0 y2)))).(let
-H_y \def (IH x2 O y1 (S y2)) in (let H2 \def (eq_ind_r nat (minus z0 O)
-(\lambda (n: nat).((le x2 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2)
-y1) (plus n (S y2))) \to (eq nat (plus x2 (S y2)) y1))))) H_y z0 (minus_n_O
-z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y2)) (\lambda (n: nat).((le x2
-z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) n) \to (eq nat (plus
-x2 (S y2)) y1))))) H2 (S (plus z0 y2)) (plus_n_Sm z0 y2)) in (let H4 \def
-(eq_ind_r nat (plus x2 (S y2)) (\lambda (n: nat).((le x2 z0) \to ((le O z0)
-\to ((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))) \to (eq nat n y1)))))
-H3 (S (plus x2 y2)) (plus_n_Sm x2 y2)) in (H4 (le_S_n x2 z0 H) (le_O_n z0)
-H1)))))))))) (\lambda (x4: nat).(\lambda (_: ((\forall (y1: nat).(\forall
-(y2: nat).((le (S x2) (S z0)) \to ((le x4 (S z0)) \to ((eq nat (plus (minus
-z0 x2) y1) (plus (match x4 with [O \Rightarrow (S z0) | (S l) \Rightarrow
-(minus z0 l)]) y2)) \to (eq nat (S (plus x2 y2)) (plus x4
-y1))))))))).(\lambda (y1: nat).(\lambda (y2: nat).(\lambda (H: (le (S x2) (S
-z0))).(\lambda (H0: (le (S x4) (S z0))).(\lambda (H1: (eq nat (plus (minus z0
-x2) y1) (plus (minus z0 x4) y2))).(f_equal nat nat S (plus x2 y2) (plus x4
-y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3))))
-x1)))) z).
+nat (plus n y3) (plus n y4)) \to (eq nat y4 y3))))))) in (let TMP_722 \def
+(minus_n_O z0) in (let H2 \def (eq_ind_r nat TMP_724 TMP_723 H_y z0 TMP_722)
+in (let TMP_729 \def (le_O_n z0) in (let TMP_728 \def (le_O_n z0) in (let
+TMP_726 \def (plus z0 y1) in (let TMP_725 \def (plus z0 y2) in (let TMP_727
+\def (eq_add_S TMP_726 TMP_725 H1) in (H2 y1 y2 TMP_729 TMP_728
+TMP_727)))))))))))))))) in (let TMP_721 \def (\lambda (x3: nat).(\lambda (_:
+((\forall (y1: nat).(\forall (y2: nat).((le O (S z0)) \to ((le x3 (S z0)) \to
+((eq nat (S (plus z0 y1)) (plus (match x3 with [O \Rightarrow (S z0) | (S l)
+\Rightarrow (minus z0 l)]) y2)) \to (eq nat y2 (plus x3 y1))))))))).(\lambda
+(y1: nat).(\lambda (y2: nat).(\lambda (_: (le O (S z0))).(\lambda (H0: (le (S
+x3) (S z0))).(\lambda (H1: (eq nat (S (plus z0 y1)) (plus (minus z0 x3)
+y2))).(let TMP_699 \def (S y1) in (let H_y \def (IH O x3 TMP_699) in (let
+TMP_704 \def (minus z0 O) in (let TMP_703 \def (\lambda (n: nat).(\forall
+(y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (plus n (S y1)) (plus
+(minus z0 x3) y3)) \to (let TMP_701 \def (S y1) in (let TMP_702 \def (plus x3
+TMP_701) in (eq nat y3 TMP_702)))))))) in (let TMP_700 \def (minus_n_O z0) in
+(let H2 \def (eq_ind_r nat TMP_704 TMP_703 H_y z0 TMP_700) in (let TMP_711
+\def (S y1) in (let TMP_712 \def (plus z0 TMP_711) in (let TMP_710 \def
+(\lambda (n: nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat
+n (plus (minus z0 x3) y3)) \to (let TMP_708 \def (S y1) in (let TMP_709 \def
+(plus x3 TMP_708) in (eq nat y3 TMP_709)))))))) in (let TMP_706 \def (plus z0
+y1) in (let TMP_707 \def (S TMP_706) in (let TMP_705 \def (plus_n_Sm z0 y1)
+in (let H3 \def (eq_ind_r nat TMP_712 TMP_710 H2 TMP_707 TMP_705) in (let
+TMP_717 \def (S y1) in (let TMP_718 \def (plus x3 TMP_717) in (let TMP_716
+\def (\lambda (n: nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq
+nat (S (plus z0 y1)) (plus (minus z0 x3) y3)) \to (eq nat y3 n)))))) in (let
+TMP_714 \def (plus x3 y1) in (let TMP_715 \def (S TMP_714) in (let TMP_713
+\def (plus_n_Sm x3 y1) in (let H4 \def (eq_ind_r nat TMP_718 TMP_716 H3
+TMP_715 TMP_713) in (let TMP_720 \def (le_O_n z0) in (let TMP_719 \def
+(le_S_n x3 z0 H0) in (H4 y2 TMP_720 TMP_719 H1))))))))))))))))))))))))))))))
+in (nat_ind TMP_733 TMP_730 TMP_721 x2))))) in (let TMP_698 \def (\lambda
+(x2: nat).(\lambda (_: ((\forall (x3: nat).(\forall (y1: nat).(\forall (y2:
+nat).((le x2 (S z0)) \to ((le x3 (S z0)) \to ((eq nat (plus (minus (S z0) x2)
+y1) (plus (minus (S z0) x3) y2)) \to (eq nat (plus x2 y2) (plus x3
+y1)))))))))).(\lambda (x3: nat).(let TMP_697 \def (\lambda (n: nat).(\forall
+(y1: nat).(\forall (y2: nat).((le (S x2) (S z0)) \to ((le n (S z0)) \to ((eq
+nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2)) \to (let
+TMP_695 \def (S x2) in (let TMP_696 \def (plus TMP_695 y2) in (let TMP_694
+\def (plus n y1) in (eq nat TMP_696 TMP_694)))))))))) in (let TMP_693 \def
+(\lambda (y1: nat).(\lambda (y2: nat).(\lambda (H: (le (S x2) (S
+z0))).(\lambda (_: (le O (S z0))).(\lambda (H1: (eq nat (plus (minus z0 x2)
+y1) (S (plus z0 y2)))).(let TMP_671 \def (S y2) in (let H_y \def (IH x2 O y1
+TMP_671) in (let TMP_676 \def (minus z0 O) in (let TMP_675 \def (\lambda (n:
+nat).((le x2 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) (plus n
+(S y2))) \to (let TMP_673 \def (S y2) in (let TMP_674 \def (plus x2 TMP_673)
+in (eq nat TMP_674 y1))))))) in (let TMP_672 \def (minus_n_O z0) in (let H2
+\def (eq_ind_r nat TMP_676 TMP_675 H_y z0 TMP_672) in (let TMP_683 \def (S
+y2) in (let TMP_684 \def (plus z0 TMP_683) in (let TMP_682 \def (\lambda (n:
+nat).((le x2 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) n) \to
+(let TMP_680 \def (S y2) in (let TMP_681 \def (plus x2 TMP_680) in (eq nat
+TMP_681 y1))))))) in (let TMP_678 \def (plus z0 y2) in (let TMP_679 \def (S
+TMP_678) in (let TMP_677 \def (plus_n_Sm z0 y2) in (let H3 \def (eq_ind_r nat
+TMP_684 TMP_682 H2 TMP_679 TMP_677) in (let TMP_689 \def (S y2) in (let
+TMP_690 \def (plus x2 TMP_689) in (let TMP_688 \def (\lambda (n: nat).((le x2
+z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))) \to
+(eq nat n y1))))) in (let TMP_686 \def (plus x2 y2) in (let TMP_687 \def (S
+TMP_686) in (let TMP_685 \def (plus_n_Sm x2 y2) in (let H4 \def (eq_ind_r nat
+TMP_690 TMP_688 H3 TMP_687 TMP_685) in (let TMP_692 \def (le_S_n x2 z0 H) in
+(let TMP_691 \def (le_O_n z0) in (H4 TMP_692 TMP_691
+H1)))))))))))))))))))))))))))) in (let TMP_670 \def (\lambda (x4:
+nat).(\lambda (_: ((\forall (y1: nat).(\forall (y2: nat).((le (S x2) (S z0))
+\to ((le x4 (S z0)) \to ((eq nat (plus (minus z0 x2) y1) (plus (match x4 with
+[O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)]) y2)) \to (eq nat (S
+(plus x2 y2)) (plus x4 y1))))))))).(\lambda (y1: nat).(\lambda (y2:
+nat).(\lambda (H: (le (S x2) (S z0))).(\lambda (H0: (le (S x4) (S
+z0))).(\lambda (H1: (eq nat (plus (minus z0 x2) y1) (plus (minus z0 x4)
+y2))).(let TMP_669 \def (plus x2 y2) in (let TMP_668 \def (plus x4 y1) in
+(let TMP_666 \def (le_S_n x2 z0 H) in (let TMP_665 \def (le_S_n x4 z0 H0) in
+(let TMP_667 \def (IH x2 x4 y1 y2 TMP_666 TMP_665 H1) in (f_equal nat nat S
+TMP_669 TMP_668 TMP_667))))))))))))) in (nat_ind TMP_697 TMP_693 TMP_670
+x3))))))) in (nat_ind TMP_737 TMP_734 TMP_698 x1))))))) in (nat_ind TMP_755
+TMP_752 TMP_738 z)))).