DEFINITION eq_nat_dec()
TYPE =
       ∀i:nat.∀j:nat.(or (not (eq nat i j)) (eq nat i j))
BODY =
       assume i: nat
          we proceed by induction on i to prove ∀j:nat.(or (not (eq nat i j)) (eq nat i j))
             case O : ⇒
                the thesis becomes ∀j:nat.(or (not (eq nat O j)) (eq nat O j))
                   assume j: nat
                      we proceed by induction on j to prove or (not (eq nat O j)) (eq nat O j)
                         case O : ⇒
                            the thesis becomes or (not (eq nat O O)) (eq nat O O)
                               by (refl_equal . .)
                               we proved eq nat O O
                               by (or_intror . . previous)
or (not (eq nat O O)) (eq nat O O)
                         case S : n:nat ⇒
                            the thesis becomes or (not (eq nat O (S n))) (eq nat O (S n))
                            () by induction hypothesis we know or (not (eq nat O n)) (eq nat O n)
                               by (O_S .)
                               we proved not (eq nat O (S n))
                               by (or_introl . . previous)
or (not (eq nat O (S n))) (eq nat O (S n))
                      we proved or (not (eq nat O j)) (eq nat O j)
∀j:nat.(or (not (eq nat O j)) (eq nat O j))
             case S : n:nat ⇒
                the thesis becomes ∀j:nat.(or (not (eq nat (S n) j)) (eq nat (S n) j))
                (H) by induction hypothesis we know ∀j:nat.(or (not (eq nat n j)) (eq nat n j))
                   assume j: nat
                      we proceed by induction on j to prove or (not (eq nat (S n) j)) (eq nat (S n) j)
                         case O : ⇒
                            the thesis becomes or (not (eq nat (S n) O)) (eq nat (S n) O)
                               by (O_S .)
                               we proved not (eq nat O (S n))
                               by (sym_not_eq . . . previous)
                               we proved not (eq nat (S n) O)
                               by (or_introl . . previous)
or (not (eq nat (S n) O)) (eq nat (S n) O)
                         case S : n0:nat ⇒
                            the thesis becomes or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))
                            () by induction hypothesis we know or (not (eq nat (S n) n0)) (eq nat (S n) n0)
                               by (H .)
                               we proved or (not (eq nat n n0)) (eq nat n n0)
                               we proceed by induction on the previous result to prove or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))
                                  case or_introl : H1:not (eq nat n n0) ⇒
                                     the thesis becomes or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))
                                        by (not_eq_S . . H1)
                                        we proved not (eq nat (S n) (S n0))
                                        by (or_introl . . previous)
or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))
                                  case or_intror : H1:eq nat n n0 ⇒
                                     the thesis becomes or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))
                                        by (f_equal . . . . . H1)
                                        we proved eq nat (S n) (S n0)
                                        by (or_intror . . previous)
or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))
or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))
                      we proved or (not (eq nat (S n) j)) (eq nat (S n) j)
∀j:nat.(or (not (eq nat (S n) j)) (eq nat (S n) j))
          we proved ∀j:nat.(or (not (eq nat i j)) (eq nat i j))
       we proved ∀i:nat.∀j:nat.(or (not (eq nat i j)) (eq nat i j))