diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 82d3e7dc89b4993f46099039d075d6860c5537c4..ac685874bb2f1aea68115dc43d0cb64e409e5009 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -946,12 +946,19 @@ Notation discrete_ofe_equivalence_of A := ltac:(
 Instance leibnizO_leibniz A : LeibnizEquiv (leibnizO A).
 Proof. by intros x y. Qed.
 
+(** * Basic Coq types *)
 Canonical Structure boolO := leibnizO bool.
 Canonical Structure natO := leibnizO nat.
 Canonical Structure positiveO := leibnizO positive.
 Canonical Structure NO := leibnizO N.
 Canonical Structure ZO := leibnizO Z.
 
+Section prop.
+  Instance Prop_equiv : Equiv Prop := iff.
+  Instance Prop_equivalence : Equivalence (≡@{PROP}) := _.
+  Canonical Structure PropO := discreteO Prop.
+End prop.
+
 (** * Option type *)
 Section option.
   Context {A : ofeT}.