Add simple notation for successor function

source/casestudies/2022-tptp/peano.mmt

@@ -4,6 +4,9 @@ theory Peano : latin:/?HOLND =
     N : tp❙
     successor : tm (N → N)❙
 
+    // simple notation for successor application ❙
+    suc = [n: tm N] (successor @ n) ❙
+
     zero : tm N❙
 
     //No Confusion Axiom❙
@@ -28,4 +31,4 @@ theory Peano : latin:/?HOLND =
     //decl2 = successor @ (successor @ zero)❙
 
     //conj2 : ⊦ ¬(decl2 =ͭ zero) ❘ = PROVE❙
-❚
\ No newline at end of file
+❚