DEFINITION plus_O()
TYPE =
       ∀x:nat
         .∀y:nat.(eq nat (plus x y) O)→(land (eq nat x O) (eq nat y O))
BODY =
       assume x: nat
          we proceed by induction on x to prove ∀y:nat.(eq nat (plus x y) O)→(land (eq nat x O) (eq nat y O))
             case O : ⇒
                the thesis becomes ∀y:nat.(eq nat (plus O y) O)→(land (eq nat O O) (eq nat y O))
                    assume y: nat
                    suppose H: eq nat (plus O y) O
                      (h1) 
                         by (refl_equal . .)
eq nat O O
                      end of h1
                      (h2) 
                         consider H
                         we proved eq nat (plus O y) O
eq nat y O
                      end of h2
                      by (conj . . h1 h2)
                      we proved land (eq nat O O) (eq nat y O)
∀y:nat.(eq nat (plus O y) O)→(land (eq nat O O) (eq nat y O))
             case S : n:nat ⇒
                the thesis becomes 
                ∀y:nat
                  .∀H0:(eq nat (plus (S n) y) O).(land (eq nat (S n) O) (eq nat y O))
                () by induction hypothesis we know ∀y:nat.(eq nat (plus n y) O)→(land (eq nat n O) (eq nat y O))
                    assume y: nat
                    suppose H0: eq nat (plus (S n) y) O
                      (H1) 
                         by cases on H0 we prove (eq nat O O)→(land (eq nat (S n) O) (eq nat y O))
                            case refl_equal ⇒
                               the thesis becomes 
                                     eq nat (plus (S n) y) O
                                       →land (eq nat (S n) O) (eq nat y O)
                               suppose H1: eq nat (plus (S n) y) O
                                  (H2) 
                                     we proceed by induction on H1 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                        case refl_equal : ⇒
                                           the thesis becomes <λ:nat.Prop> CASE plus (S n) y OF O⇒False | S ⇒True
                                              consider I
                                              we proved True
<λ:nat.Prop> CASE plus (S n) y OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                  end of H2
                                  consider H2
                                  we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                  that is equivalent to False
                                  we proceed by induction on the previous result to prove land (eq nat (S n) O) (eq nat y O)
                                  we proved land (eq nat (S n) O) (eq nat y O)

                                  eq nat (plus (S n) y) O
                                    →land (eq nat (S n) O) (eq nat y O)
(eq nat O O)→(land (eq nat (S n) O) (eq nat y O))
                      end of H1
                      by (refl_equal . .)
                      we proved eq nat O O
                      by (H1 previous)
                      we proved land (eq nat (S n) O) (eq nat y O)

                      ∀y:nat
                        .∀H0:(eq nat (plus (S n) y) O).(land (eq nat (S n) O) (eq nat y O))
          we proved ∀y:nat.(eq nat (plus x y) O)→(land (eq nat x O) (eq nat y O))
       we proved 
          ∀x:nat
            .∀y:nat.(eq nat (plus x y) O)→(land (eq nat x O) (eq nat y O))