Use telescopes for atomic triples.

program_logic/atomic.v

 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import classes.
 
-Definition atomic_shift `{invG Σ} {A B}
+Section Telescopes.
+  Inductive Tele (T : Type) : Type :=
+  | TeleB (b : T) : Tele T
+  | TeleT {X} (f : X -> Tele T) : Tele T.
+  
+  Definition Tfold {X Y} (t : Tele X) (F : ∀ A : Type, (A -> Y) -> Y) (B : X -> Y) : Y :=
+    (fix rec t :=
+      match t with
+      | TeleB b => B b
+      | TeleT _ ft => F _ (rec ∘ ft)
+      end) t.
+End Telescopes.
+Arguments Tele _%type.
+Arguments TeleB [_%type] _.
+Arguments TeleT [_ _]%type _.
+
+Definition atomic_shift `{invG Σ} {A B C}
     (Eo Ei : coPset) (* inside/outside masks *)
-    (α : A → iProp Σ) (* atomic pre-condition *)
+    (α : A → iProp Σ) (* Σatomic pre-condition *)
     (β : A → B → iProp Σ) (* atomic post-condition *)
     (P : iProp Σ)
-    (Φ : B → iProp Σ) : iProp Σ :=
-  (□ (P ={Eo,Ei}=★ ∃ x : A,
-        α x ★ ((α x ={Ei,Eo}=★ P) ∧ ∀ v, β x v ={Ei,Eo}=★ Φ v)))%I.
+    (f : A -> B -> C)
+    (Φ : C → iProp Σ) : iProp Σ :=
+  (□ (P ={Eo,Ei}=∗ ∃ x : A,
+        α x ∗ ((α x ={Ei,Eo}=∗ P) ∧ ∀ y, β x y ={Ei,Eo}=∗ Φ (f x y))))%I.
+
+Definition atomic_tele Σ C := Tele (iProp Σ * Tele (iProp Σ * C)). 
+
+Definition atomic_shift' `{invG Σ} {C}
+    (Eo Ei : coPset) (* inside/outside masks *)
+    (P : iProp Σ)
+    (Φ : C → iProp Σ)
+    (t : atomic_tele Σ C) : iProp Σ :=
+  (□ (P ={Eo,Ei}=∗
+                Tfold t
+                (@uPred_exist _)
+                (λ α_βf,
+                 α_βf.1
+                   ∗ (
+                     (α_βf.1 ={Ei,Eo}=∗ P)
+                     ∧ Tfold (α_βf.2)
+                             (@uPred_forall _)
+                             (λ β_f,
+                              β_f.1  ={Ei,Eo}=∗ Φ (β_f.2)
+                             )
+                   )
+                )
+  ))%I.
+
+Definition atomic_triple' `{irisG Λ Σ} 
+    (Eo Ei : coPset) (* inside/outside masks *)
+    (e : expr Λ)
+    (t : atomic_tele Σ (val Λ)) : iProp Σ :=
+  (∀ P Φ,
+    atomic_shift' Eo Ei P Φ t -∗
+    P -∗ WP e {{ Φ }})%I.
 
 Definition atomic_triple `{irisG Λ Σ} {A}
     (Eo Ei : coPset) (* inside/outside masks *)
@@ -16,8 +64,8 @@ Definition atomic_triple `{irisG Λ Σ} {A}
     (e : expr Λ)
     (β : A → val Λ → iProp Σ) : iProp Σ := (* atomic post-condition *)
   (□ ∀ P Φ,
-    atomic_shift Eo Ei α β P Φ -★
-    P -★ WP e {{ Φ }})%I.
+    atomic_shift Eo Ei α β P Φ -∗
+    P -∗ WP e {{ Φ }})%I.
 
 Notation "⟨⟨ x , α ⟩ ⟩ e @ Eo , Ei ⟨⟨ v , β ⟩ ⟩" :=
   (atomic_triple Eo Ei (λ x, α) e%E (λ x v, β))