diff --git a/algebra/upred.v b/algebra/upred.v
index 096ca4dd2c33899bc0a52fd387b04ac22dfa8901..d3ddbbcd8b39c22bb66c40ecfc6117a712fbfe68 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1492,11 +1492,11 @@ Proof.
   eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
 Qed.
 
-Corollary consistencyModal n : ¬ (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) False).
+Corollary consistency_modal n : ¬ (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) False).
 Proof. exact (adequacy False n). Qed.
 
 Corollary consistency : ¬ (True ⊢ False).
-Proof. exact (consistencyModal 0). Qed.
+Proof. exact (consistency_modal 0). Qed.
 End uPred_logic.
 
 (* Hint DB for the logic *)
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 989a0e7f918ec4c15b3755d2dd88e8c68908c637..e74f5a254a06fa8ffa07728061081eb62b099ea3 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -130,7 +130,7 @@ The fragment will then be available to the user of the logic, as their way of ta
 It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs on paper.
 Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple:
 \[
-\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\lambda\Ret\val.\propB})}
+\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\Ret\val.\propB})}
 \]
 
 \subsection{Lost stuff}