diff --git a/personoj/coercions.lp b/personoj/coercions.lp
index 9296312cd5b4d96b9604a43ffe42662b24eb2500..0c6c9594e35bd8c52bd8fab16f0a68dbc1fc7255 100644
--- a/personoj/coercions.lp
+++ b/personoj/coercions.lp
@@ -33,7 +33,7 @@ with c : El t → El u;
 require personoj.extra.arity-tools as A;
 coercion "tup-cons"
   (a a': Set) (n: A.N) (v v': SVec n) (arg: El (@σ (A.s n) (@& n a v))) ⊢
-  @argS n a' v' $c[@head (A.s n) a arg] $d[@tail n v arg]:
+  @^ n a' v' $c[@head (A.s n) a arg] $d[@tail n v arg]:
   El (@σ (A.s n) (@& n a' v'))
  on 6
  with c: El a → El a'
diff --git a/personoj/eqtup.lp b/personoj/eqtup.lp
index 45c939e800736fb01370981458beb5e95fb6cf27..4f043f0e880cb3d9d3919a635e0c9b00131ccc4e 100644
--- a/personoj/eqtup.lp
+++ b/personoj/eqtup.lp
@@ -6,6 +6,6 @@ require open personoj.lhol personoj.pvs_cert personoj.tuple personoj.logical;
 symbol eq {t: Set} (_: El (σ (t & t & &nil))): Prop;
 // Equality operates on the maximal supertype. It allows to profit
 // from predicate subtyping for free in the propositional equality.
-rule @eq (@psub $t $p) (argS $x (argS $y arg0))
-   ↪ @eq $t (argS (@fst $t $p $x) (argS (@fst $t $p $y) arg0));
+rule @eq (@psub $t $p) ($x ^ $y ^ ^nil)
+   ↪ @eq $t ((@fst $t $p $x) ^ (@fst $t $p $y) ^ ^nil);
 symbol neq {t} m ≔ ¬ (@eq t m);
diff --git a/personoj/examples/transitivity.lp b/personoj/examples/transitivity.lp
index 5b014d93efbeeb566be131a4fdbbba7063e02be0..553357cce0937ac7b4361fc943eec1e5e85adbb8 100644
--- a/personoj/examples/transitivity.lp
+++ b/personoj/examples/transitivity.lp
@@ -35,5 +35,5 @@ begin admit; end;
 
 // With a tuple
 symbol bar: El (σ (numfield & numfield* & &nil)) → Prop;
-symbol barx : Π x: El real, Π y: El real*, Prf (bar (argS x (argS y arg0)))
+symbol barx : Π x: El real, Π y: El real*, Prf (bar (x ^ y ^ ^nil))
 begin admit; end;
diff --git a/personoj/extra/bool_plus.lp b/personoj/extra/bool_plus.lp
index bea982fb51b06a7e9db510567c7601a107b01333..1e94967ca6e8c0435e66658a77113b589385b9f6 100644
--- a/personoj/extra/bool_plus.lp
+++ b/personoj/extra/bool_plus.lp
@@ -19,4 +19,4 @@ admitted;
 
 symbol propositional_extensionality:
   Prf (∀ (λ p: El prop,
-          (∀ (λ q: El prop, (iff p q) ⇒ (λ _, eq (argS p (argS q arg0)))))));
+          (∀ (λ q: El prop, (iff p q) ⇒ (λ _, eq (p ^ q ^ ^nil))))));
diff --git a/personoj/tuple.lp b/personoj/tuple.lp
index aebfc3b67e5e5f93160060082053c1fbf03ed529..7644451d039f365efb8e98bed32649717a71d0a4 100644
--- a/personoj/tuple.lp
+++ b/personoj/tuple.lp
@@ -19,14 +19,15 @@ injective symbol mkarr {n: N}: SVec n → Set → Set;
 rule mkarr &nil $Ret ↪ $Ret
 with mkarr ($X & $Q) $Ret ↪ arr $X (mkarr $Q $Ret);
 
-constant symbol arg0 : El (σ &nil);
-constant symbol argS {n: N} {a: Set} {v: SVec n}:
+constant symbol ^ {n: N} {a: Set} {v: SVec n}:
   El a → El (σ v) → El (σ (a & v));
+constant symbol ^nil : El (σ &nil);
+notation ^ infix right 10;
 
 symbol match {l: N} {v: SVec l} (ret: Set) (arg: El (σ v)):
   El (mkarr v ret) → El ret;
-rule match {z} {&nil} _ arg0 $e ↪ $e
-with match $Ret (argS $x $y) $f ↪ match $Ret $y ($f $x);
+rule match {z} {&nil} _ ^nil $e ↪ $e
+with match $Ret ($x ^ $y) $f ↪ match $Ret $y ($f $x);
 
 /// Accessors
 
@@ -35,7 +36,7 @@ with match $Ret (argS $x $y) $f ↪ match $Ret $y ($f $x);
    have the same interface as telescopes. */
 symbol nth {n: N} (_: N) (v: SVec n) (_: El (σ v)): Set;
 rule nth z ($x & _) _ ↪ $x
-with nth (s $n) (_ & $tl) (argS _ $y) ↪ nth $n $tl $y;
+with nth (s $n) (_ & $tl) (_ ^ $y) ↪ nth $n $tl $y;
 
 symbol car {n: N}: SVec n → Set;
 rule car ($x & _) ↪ $x;
@@ -44,12 +45,12 @@ rule cdr (_ & $x) ↪ $x;
 symbol cadr {n: N} (v: SVec (s n)): Set ≔ car (cdr v);
 
 symbol argn {l: N} {v: SVec l} (n: N) (arg: El (σ v)): El (nth n v arg);
-rule argn z (argS $x _) ↪ $x
-with argn (s $n) (argS _ $Y) ↪ argn $n $Y;
+rule argn z ($x ^ _) ↪ $x
+with argn (s $n) (_ ^ $Y) ↪ argn $n $Y;
 
 /// Low level accessors
 
 symbol head {l: N} {v: SVec l} (arg: El (σ v)): El (car v);
-rule head (argS $x _) ↪ $x;
+rule head ($x ^ _) ↪ $x;
 symbol tail {l: N} {v: SVec (s l)}: El (σ v) → El (σ (cdr v));
-rule tail (argS _ $y) ↪ $y;
+rule tail (_ ^ $y) ↪ $y;