DEFINITION simpl_plus_l()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(eq nat (plus n m) (plus n p))→(eq nat m p)
BODY =
       assume n: nat
          we proceed by induction on n to prove ∀m:nat.∀p:nat.(eq nat (plus n m) (plus n p))→(eq nat m p)
             case O : ⇒
                the thesis becomes ∀m:nat.∀p:nat.(eq nat (plus O m) (plus O p))→(eq nat m p)
                    assume m: nat
                    assume p: nat
                      we must prove (eq nat (plus O m) (plus O p))→(eq nat m p)
                      or equivalently (eq nat m p)→(eq nat m p)
                      suppose H: eq nat m p
                         consider H
                      we proved (eq nat m p)→(eq nat m p)
                      that is equivalent to (eq nat (plus O m) (plus O p))→(eq nat m p)
∀m:nat.∀p:nat.(eq nat (plus O m) (plus O p))→(eq nat m p)
             case S : n0:nat ⇒
                the thesis becomes 
                ∀m:nat.∀p:nat.(eq nat (plus (S n0) m) (plus (S n0) p))→(eq nat m p)
                (IHn) by induction hypothesis we know ∀m:nat.∀p:nat.(eq nat (plus n0 m) (plus n0 p))→(eq nat m p)
                    assume m: nat
                    assume p: nat
                      we must prove (eq nat (plus (S n0) m) (plus (S n0) p))→(eq nat m p)
                      or equivalently (eq nat (S (plus n0 m)) (S (plus n0 p)))→(eq nat m p)
                      suppose H: eq nat (S (plus n0 m)) (S (plus n0 p))
                         by (eq_add_S . . H)
                         we proved eq nat (plus n0 m) (plus n0 p)
                         by (f_equal . . . . . previous)
                         we proved eq nat (plus n0 (plus n0 m)) (plus n0 (plus n0 p))
                         by (IHn . . previous)
                         we proved eq nat (plus n0 m) (plus n0 p)
                         by (IHn . . previous)
                         we proved eq nat m p
                      we proved (eq nat (S (plus n0 m)) (S (plus n0 p)))→(eq nat m p)
                      that is equivalent to (eq nat (plus (S n0) m) (plus (S n0) p))→(eq nat m p)

                      ∀m:nat.∀p:nat.(eq nat (plus (S n0) m) (plus (S n0) p))→(eq nat m p)
          we proved ∀m:nat.∀p:nat.(eq nat (plus n m) (plus n p))→(eq nat m p)
       we proved ∀n:nat.∀m:nat.∀p:nat.(eq nat (plus n m) (plus n p))→(eq nat m p)