diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 63eeb95151bd13974a5ca41edf28e9eb3274150d..89eecadc222bafd855ff6b769738b6fc903866e0 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -1043,15 +1043,6 @@ Section proto.
     by rewrite own_op.
   Qed.
 
-  (* TODO: Move somewhere else *)
-  Lemma false_disj_cong (P Q Q' : iProp Σ) :
-    (P ⊢ False) → (Q ⊣⊢ Q') → (P ∨ Q ⊣⊢ Q').
-  Proof. intros HP ->. apply (anti_symm _). by rewrite HP left_id. auto. Qed.
-
-  Lemma pure_sep_cong (φ1 φ2 : Prop) (P1 P2 : iProp Σ) :
-    (φ1 ↔ φ2) → (φ1 → φ2 → P1 ⊣⊢ P2) → (⌜φ1⌝ ∗ P1) ⊣⊢ (⌜φ2⌝ ∗ P2).
-  Proof. intros -> HP. iSplit; iDestruct 1 as (HÏ•) "H"; rewrite HP; auto. Qed.
-
   Lemma iProto_interp_nil p : ⊢ iProto_interp [] [] p (iProto_dual p).
   Proof. iExists p; simpl. iSplitL; iApply iProto_le_refl. Qed.