diff --git a/src/lib/reif.pl b/src/lib/reif.pl
index 55618e84e..6eaa86e1d 100644
--- a/src/lib/reif.pl
+++ b/src/lib/reif.pl
@@ -1,5 +1,12 @@
 /** Predicates from [*Indexing dif/2*](https://arxiv.org/abs/1607.01590).
 
+The core trick that, unlike the traditional conditional `A -> B ; C`,
+the branching condition is *not* provided as a complete goal.
+
+Rather, the branching condition is a "reified goal",
+i.e. a term which is completed with an additional argument `T`,
+representing its satisfaction (`T = true`) and refutation (`T = false`).
+
 Example:
 
 ```
@@ -19,6 +26,15 @@
 
 :- meta_predicate(if_(1, 0, 0)).
 
+%% if_(Cond_1, IfTrue, IfFalse).
+% Monotonic if-then-else construct.
+%
+% Unlike `Cond_0 -> IfTrue; IfFalse`, this is nondeterministic in the condition.
+% `Cond` is expected to be a reified goal.
+% e.g. `if_((A=1), _, _)`
+% where the `=` above is NOT the `(=)/2` predicate, but rather the `(=)/3` predicate
+% defined in this module.
+
 if_(If_1, Then_0, Else_0) :-
     call(If_1, T),
     (  T == true  -> call(Then_0)
@@ -27,6 +43,14 @@
     ;  throw(error(instantiation_error, _))
     ).
 
+%% =(X, Y, T).
+% Reified equality predicate.
+%
+% `=(X,Y,true)` succeeds if X, Y *could* unify
+% `=(X,Y,false)` succeeds if X, Y *could* fail to unify
+% Partially call as a branching condition in `if_/3`:
+%   `if_(A=B, IfTrue, IfFalse)`
+
 =(X, Y, T) :-
     (  X == Y -> T = true
     ;  X \= Y -> T = false
@@ -34,6 +58,14 @@
     ;  T = false, dif(X, Y)
     ).
 
+%% dif(X, Y, T).
+% Reified disequality predicate.
+%
+% `dif(X,Y,true)` succeeds if X, Y *could* fail to unify
+% `dif(X,Y,false)` succeeds if X, Y *could* unify
+% Partially call as a branching condition in `if_/3`:
+%   `if_(dif(A,B), IfTrue, IfFalse)`
+
 dif(X, Y, T) :-
   =(X, Y, NT),
   non(NT, T).