diff --git a/doc/org/tut04.org b/doc/org/tut04.org
index 536eff066..d6c268b2e 100644
--- a/doc/org/tut04.org
+++ b/doc/org/tut04.org
@@ -36,23 +36,21 @@ familiar to =grep= users.)
 
 * Python
 
-In Python, we can test this via a =language_containment_checker=
-object:
+In Python, we can implement this in a number of ways.  The
+easiest is to use the =spot.are_equivalent()= function.
 
 #+BEGIN_SRC python :results output :exports both
 import spot
-f = spot.formula("(a U b) U a")
-g = spot.formula("b U a")
-c = spot.language_containment_checker()
-print("Equivalent" if c.equal(f, g) else "Not equivalent")
+are_eq = spot.are_equivalent("(a U b) U a", "b U a")
+print("Equivalent" if are_eq else "Not equivalent")
 #+END_SRC
 #+RESULTS:
 : Equivalent
 
-The equivalence check is done by converting the formulas $f$ and $g$
-and their negation into four automata $A_f$, $A_{\lnot f}$, $A_g$, and
-$A_{\lnot g}$, and then making sure that $A_f\otimes A_{\lnot g}$ and
-$A_g\otimes A_{\lnot f}$ are empty.
+The equivalence check is done by converting the input formulas $f$ and
+$g$ and their negation into four automata $A_f$, $A_{\lnot f}$, $A_g$,
+and $A_{\lnot g}$, and then making sure that $A_f\otimes A_{\lnot g}$
+and $A_g\otimes A_{\lnot f}$ are empty.
 
 We could also write this check by doing [[file:tut10.org][the translation]] and emptiness
 check ourselves.  For instance:
@@ -62,7 +60,7 @@ import spot
 
 def implies(f, g):
     a_f = f.translate()
-    a_ng = spot.formula_Not(g).translate()
+    a_ng = spot.formula.Not(g).translate()
     return spot.product(a_f, a_ng).is_empty()
 
 def equiv(f, g):
@@ -75,6 +73,19 @@ print("Equivalent" if equiv(f, g) else "Not equivalent")
 #+RESULTS:
 : Equivalent
 
+
+This can also be done via a =language_containment_checker= object:
+
+#+BEGIN_SRC python :results output :exports both
+import spot
+f = spot.formula("(a U b) U a")
+g = spot.formula("b U a")
+c = spot.language_containment_checker()
+print("Equivalent" if c.equal(f, g) else "Not equivalent")
+#+END_SRC
+#+RESULTS:
+: Equivalent
+
 The =language_containment_checker= object essentially performs the
 same work, but it also implements a cache to avoid translating the
 same formulas multiple times when it is used to test multiple
@@ -82,7 +93,25 @@ equivalences.
 
 * C++
 
-Here is a C++ translation of the first Python example.
+Here are possible C++ implementations using either =are_equivalent()=
+or the =language_containment_checker=.  Note that the
+=are_equivalent()= function also work with automata.
+
+#+BEGIN_SRC C++ :results verbatim :exports both
+#include <iostream>
+#include <spot/tl/parse.hh>
+#include <spot/twaalgos/contains.hh>
+
+int main()
+{
+  spot::formula f = spot::parse_formula("(a U b) U a");
+  spot::formula g = spot::parse_formula("b U a");
+  std::cout << (spot::are_equivalent(f, g) ?
+                "Equivalent\n" : "Not equivalent\n");
+}
+#+END_SRC
+#+RESULTS:
+: Equivalent
 
 #+BEGIN_SRC C++ :results verbatim :exports both
   #include <iostream>