diff --git a/_CoqProject b/_CoqProject
index f671907c1e137f9cc5ccb230244a79c962f35305..1ff1ee86ecf91feccb32341d58118264afb0171a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -85,6 +85,7 @@ program_logic/auth.v
 program_logic/sts.v
 program_logic/namespaces.v
 program_logic/boxes.v
+program_logic/counter_examples.v
 heap_lang/lang.v
 heap_lang/tactics.v
 heap_lang/wp_tactics.v
diff --git a/algebra/upred.v b/algebra/upred.v
index 878761a858704ccc5acaf0f347f3fafd310b51bc..629b0e223a5cfad772566d7b802b066758a2f016 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -345,11 +345,18 @@ Proof.
 Qed.
 Global Instance: AntiSymm (⊣⊢) (@uPred_entails M).
 Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
+
+Lemma sound : ¬ (True ⊢ False).
+Proof.
+  unseal. intros [H]. apply (H 0 ∅); last done. apply ucmra_unit_validN.
+Qed.
+
 Lemma equiv_spec P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
 Proof.
   split; [|by intros [??]; apply (anti_symm (⊢))].
   intros HPQ; split; split=> x i; apply HPQ.
 Qed.
+
 Lemma equiv_entails P Q : (P ⊣⊢ Q) → (P ⊢ Q).
 Proof. apply equiv_spec. Qed.
 Lemma equiv_entails_sym P Q : (Q ⊣⊢ P) → (P ⊢ Q).
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
new file mode 100644
index 0000000000000000000000000000000000000000..894359c3ee707199653290f61e4492f3deb7151c
--- /dev/null
+++ b/program_logic/counter_examples.v
@@ -0,0 +1,70 @@
+From iris.algebra Require Import upred.
+From iris.proofmode Require Import tactics.
+
+(** This proves that we need the â–· in a "Saved Proposition" construction with
+    name-dependend allocation. *)
+(** We fork in [uPred M] for any M, but the proof would work in any BI. *)
+Section savedprop.
+  Context (M : ucmraT).
+  Notation iProp := (uPred M).
+  Notation "¬ P" := (□(P → False))%I : uPred_scope.
+
+  (* Saved Propositions. *)
+  Context (sprop : Type) (saved : sprop → iProp → iProp).
+  Hypothesis sprop_persistent : forall i P, PersistentP (saved i P).
+  Hypothesis sprop_alloc_dep :
+    forall (P : sprop → iProp), True ⊢ ∃ i, saved i (P i).
+  Hypothesis sprop_agree :
+    forall i P Q, saved i P ∧ saved i Q ⊢ P ↔ Q.
+
+  (* Self-contradicting assertions are inconsistent *)
+  Lemma no_self_contradiction (P : iProp) `{!PersistentP P} :
+    □(P ↔ ¬ P) ⊢ False.
+  Proof. (* FIXME: Cannot destruct the <-> as two implications. iApply with <-> also does not work. *)
+    rewrite /uPred_iff. iIntros "#[H1 H2]". (* FIXME: Cannot iApply "H1". *)
+    iAssert P as "#HP".
+    { iApply "H2". iIntros "!#HP". by iApply ("H1" with "HP"). }
+    by iApply ("H1" with "HP HP").
+  Qed.
+
+  (* "Assertion with name [i]" is equivalent to any assertion P s.t. [saved i P] *)
+  Definition A (i : sprop) : iProp := ∃ P, saved i P ★ □P.
+  Lemma saved_is_A i P `{!PersistentP P} : saved i P ⊢ □(A i ↔ P).
+  Proof.
+    rewrite /uPred_iff. iIntros "#HS !". iSplit.
+    - iIntros "H". iDestruct "H" as (Q) "[#HSQ HQ]".
+      iPoseProof (sprop_agree i P Q with "[]") as "Heq"; first by eauto.
+      rewrite /uPred_iff. by iApply "Heq".
+    - iIntros "#HP". iExists P. by iSplit.
+  Qed.
+
+  (* Define [Q i] to be "negated assertion with name [i]". Show that this
+     implies that assertion with name [i] is equivalent to its own negation. *)
+  Definition Q i := saved i (¬ A i).
+  Lemma Q_self_contradiction i :
+    Q i ⊢ □(A i ↔ ¬ A i).
+  Proof.
+    iIntros "#HQ". iApply (@saved_is_A i (¬ A i)%I _). (* FIXME: If we already introduced the box, this iApply does not work. *)
+    done.
+  Qed.
+
+  (* We can obtain such a [Q i]. *)
+  Lemma make_Q :
+    True ⊢ ∃ i, Q i.
+  Proof.
+    apply sprop_alloc_dep.
+  Qed.
+
+  (* Put together all the pieces to derive a contradiction. *)
+  Lemma contradiction : False.
+  Proof.
+    apply (@uPred.sound M). iIntros "".
+    iPoseProof make_Q as "HQ". iDestruct "HQ" as (i) "HQ".
+    iApply (@no_self_contradiction (A i) _).
+    by iApply Q_self_contradiction.
+  Qed.
+End savedprop.
+
+
+  
+