diff --git a/algebra/dra.v b/algebra/dra.v
index f62020e4bd4798410a6c9e8cc6d72e4124691950..b2a0439d0b948ea68d610656da4094f6833fe2f7 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -127,6 +127,7 @@ Lemma to_validity_op (x y : A) :
   to_validity (x ⋅ y) ≡ to_validity x ⋅ to_validity y.
 Proof. split; naive_solver auto using dra_op_valid. Qed.
 
+(* TODO: This has to be proven again. *)
 (*
 Lemma to_validity_included x y:
   (✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y).
diff --git a/algebra/sts.v b/algebra/sts.v
index e35b4206c84e396023b4a38b02d862a6f5d8e23f..dccd85d5da0b4eb77ab70fde8ad98437ec9947b1 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -385,6 +385,7 @@ Qed.
 (* This is surprisingly different from to_validity_included. I am not sure
    whether this is because to_validity_included is non-canonical, or this
    one here is non-canonical - but I suspect both. *)
+(* TODO: These have to be proven again. *)
 (*
 Lemma sts_frag_included S1 S2 T1 T2 :
   closed S2 T2 → S2 ≢ ∅ →