enrich nat with functions . * . : Nat × Nat → Nat prio 10 right; variables m : Nat; n : Nat; axioms mult-base: m * 0 = 0; mult-rec: m * n +1 = m * n + m; end enrich