diff --git a/examples/nqueens/NQueens.gf b/examples/nqueens/NQueens.gf
index 04aa96a80..bcef1db5c 100644
--- a/examples/nqueens/NQueens.gf
+++ b/examples/nqueens/NQueens.gf
@@ -6,13 +6,13 @@ cat Vec (s,l : Nat) Constr ;
 cat Sat Nat Nat Constr ;
 
 data nilV  : (s : Nat) -> (c : Constr) -> Vec s zero c ;
-     consV : (s,l : Nat) -> (j : Nat) -> (c : Constr) -> LT j s -> Sat j (succ zero) c -> Vec s l (consC j c) -> Vec s (succ l) c ;
+     consV : (s,l,j : Nat) -> (c : Constr) -> LT j s -> Sat j (succ zero) c -> Vec s l (consC j c) -> Vec s (succ l) c ;
 
      nilC  : Constr ;
      consC : (j : Nat) -> Constr -> Constr ;
 
      nilS : (j,d : Nat) -> Sat j d nilC ;
-     consS : (i,j : Nat) -> (d,dj,di : Nat) -> (c : Constr) -> NE i j -> Plus d j dj -> Plus d i di -> NE i dj -> NE di j -> Sat j (succ d) c -> Sat j d (consC i c) ;
+     consS : (i,j,d : Nat) -> (c : Constr) -> NE i j -> NE i (plus d j) -> NE (plus d i) j -> Sat j (succ d) c -> Sat j d (consC i c) ;
 
      matrix : (s : Nat) -> Vec s s nilC -> Matrix s ;
 
diff --git a/examples/nqueens/Nat.gf b/examples/nqueens/Nat.gf
index 8c8b5d542..d53dc10ac 100644
--- a/examples/nqueens/Nat.gf
+++ b/examples/nqueens/Nat.gf
@@ -7,7 +7,6 @@ data zero : Nat ;
 
 cat NE (i,j : Nat) ;
 cat LT (i,j : Nat) ;
-cat Plus Nat Nat Nat ;
 
 data zNE : (i,j : Nat) -> NE i j -> NE (succ i) (succ j) ;
      lNE : (j : Nat) -> NE zero (succ j) ;
@@ -16,7 +15,8 @@ data zNE : (i,j : Nat) -> NE i j -> NE (succ i) (succ j) ;
      zLT : (n : Nat) -> LT zero (succ n) ;
      sLT : (m,n : Nat) -> LT m n -> LT (succ m) (succ n) ;
 
-     zP : (n : Nat) -> Plus zero n n ;
-     sP : (m,n,s : Nat) -> Plus m n s -> Plus (succ m) n (succ s) ;
+fun plus : Nat -> Nat -> Nat ;
+def plus zero     n = n ;
+    plus (succ m) n = succ (plus m n) ;
 
 }
\ No newline at end of file
diff --git a/examples/nqueens/NatAscii.gf b/examples/nqueens/NatAscii.gf
index 26f6533ea..5c0892d66 100644
--- a/examples/nqueens/NatAscii.gf
+++ b/examples/nqueens/NatAscii.gf
@@ -7,7 +7,6 @@ lin zero   = "" ;
 
 lincat LT = Str ;
        NE = {} ;
-       Plus = {} ;
 
 lin zLT n = n ;
     sLT _ _ l = l ;