DEFINITION plus_sym()
TYPE =
       ∀n:nat.∀m:nat.(eq nat (plus n m) (plus m n))
BODY =
        assume n: nat
        assume m: nat
          we proceed by induction on n to prove eq nat (plus n m) (plus m n)
             case O : ⇒
                the thesis becomes eq nat (plus O m) (plus m O)
                   by (plus_n_O .)
                   we proved eq nat m (plus m O)
eq nat (plus O m) (plus m O)
             case S : y:nat ⇒
                the thesis becomes eq nat (plus (S y) m) (plus m (S y))
                (H) by induction hypothesis we know eq nat (plus y m) (plus m y)
                   by (plus_n_Sm . .)
                   we proved eq nat (S (plus m y)) (plus m (S y))
                   we proceed by induction on the previous result to prove eq nat (S (plus y m)) (plus m (S y))
                      case refl_equal : ⇒
                         the thesis becomes eq nat (S (plus y m)) (S (plus m y))
                            by (f_equal . . . . . H)
eq nat (S (plus y m)) (S (plus m y))
                   we proved eq nat (S (plus y m)) (plus m (S y))
eq nat (plus (S y) m) (plus m (S y))
          we proved eq nat (plus n m) (plus m n)
       we proved ∀n:nat.∀m:nat.(eq nat (plus n m) (plus m n))