diff --git a/iface/ltsmin/ltsmin.cc b/iface/ltsmin/ltsmin.cc
index dc5b1d8ef..44abec4d4 100644
--- a/iface/ltsmin/ltsmin.cc
+++ b/iface/ltsmin/ltsmin.cc
@@ -647,12 +647,12 @@ namespace spot
 	// appropriately.  ALIVE_PROP is the bdd that should be ANDed
 	// to all transitions leaving a live state, while DEAD_PROP should
 	// be ANDed to all transitions leaving a dead state.
-	if (dead.is_false())
+	if (dead.is_ff())
 	  {
 	    alive_prop = bddtrue;
 	    dead_prop = bddfalse;
 	  }
-	else if (dead.is_true())
+	else if (dead.is_tt())
 	  {
 	    alive_prop = bddtrue;
 	    dead_prop = bddtrue;
diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc
index 4c2788de5..4b73c62e4 100644
--- a/src/ltlast/formula.cc
+++ b/src/ltlast/formula.cc
@@ -138,7 +138,7 @@ namespace spot
     void
     fnode::destroy_aux() const
     {
-      if (SPOT_UNLIKELY(is(op::AP)))
+      if (SPOT_UNLIKELY(is(op::ap)))
 	{
 	  auto i = m.ap2name.find(id());
 	  auto n = m.name2ap.erase(i->second);
@@ -165,10 +165,10 @@ namespace spot
 	case op::x:				\
 	  return #x;				\
 	  break
-	  C(False);
-	  C(True);
-	  C(EmptyWord);
-	  C(AP);
+	  C(ff);
+	  C(tt);
+	  C(eword);
+	  C(ap);
 	  C(Not);
 	  C(X);
 	  C(F);
@@ -618,7 +618,7 @@ namespace spot
       //   - 0[*min..max] = 0 if min > 0
       //   - b[:*0..max] = 1
       //   - b[:*min..max] = 0 if min > 0
-      if (child->is_false()
+      if (child->is_ff()
 	  || (o == op::FStar && child->is_boolean()))
 	{
 	  if (min == 0)
@@ -709,7 +709,7 @@ namespace spot
 
 	    // F(0) = G(0) = 0
 	    // F(1) = G(1) = 1
-	    if (f->is_false() || f->is_true())
+	    if (f->is_ff() || f->is_tt())
 	      return f;
 
 	    assert(!f->is_eword());
@@ -719,10 +719,10 @@ namespace spot
 	case op::Not:
 	  {
 	    // !1 = 0
-	    if (f->is_true())
+	    if (f->is_tt())
 	      return ff();
 	    // !0 = 1
-	    if (f->is_false())
+	    if (f->is_ff())
 	      return tt();
 	    // ![*0] = 1[+]
 	    if (f->is_eword())
@@ -754,7 +754,7 @@ namespace spot
 	  }
 	case op::X:
 	  // X(1) = 1,  X(0) = 0
-	  if (f->is_true() || f->is_false())
+	  if (f->is_tt() || f->is_ff())
 	    return f;
 	  assert(!f->is_eword());
 	  break;
@@ -771,10 +771,10 @@ namespace spot
 	case op::NegClosure:
 	case op::NegClosureMarked:
 	  // {1} = 0
-	  if (f->is_true())
+	  if (f->is_tt())
 	    return ff();
 	  // {0} = 1,  {[*0]} = 1
-	  if (f->is_false() || f->is_eword())
+	  if (f->is_ff() || f->is_eword())
 	    return tt();
 	  // {b} = !b
 	  if (f->is_boolean())
@@ -806,9 +806,9 @@ namespace spot
 	  }
 	  //   - (1 ^ Exp) = !Exp
 	  //   - (0 ^ Exp) = Exp
-	  if (first->is_true())
+	  if (first->is_tt())
 	    return unop(op::Not, second);
-	  if (first->is_false())
+	  if (first->is_ff())
 	    return second;
 	  if (first == second)
 	    {
@@ -830,9 +830,9 @@ namespace spot
 	  //   - (0 <=> Exp) = !Exp
 	  //   - (1 <=> Exp) = Exp
 	  //   - (Exp <=> Exp) = 1
-	  if (first->is_false())
+	  if (first->is_ff())
 	    return unop(op::Not, second);
-	  if (first->is_true())
+	  if (first->is_tt())
 	    return second;
 	  if (first == second)
 	    {
@@ -850,19 +850,19 @@ namespace spot
 	  //   - (Exp => 1) = 1
 	  //   - (Exp => 0) = !Exp
 	  //   - (Exp => Exp) = 1
-	  if (first->is_true())
+	  if (first->is_tt())
 	    return second;
-	  if (first->is_false())
+	  if (first->is_ff())
 	    {
 	      second->destroy();
 	      return tt();
 	    }
-	  if (second->is_true())
+	  if (second->is_tt())
 	    {
 	      first->destroy();
 	      return second;
 	    }
-	  if (second->is_false())
+	  if (second->is_ff())
 	    return unop(op::Not, first);
 	  if (first == second)
 	    {
@@ -876,9 +876,9 @@ namespace spot
 	  //   - (Exp U 0) = 0
 	  //   - (0 U Exp) = Exp
 	  //   - (Exp U Exp) = Exp
-	  if (second->is_true()
-	      || second->is_false()
-	      || first->is_false()
+	  if (second->is_tt()
+	      || second->is_ff()
+	      || first->is_ff()
 	      || first == second)
 	    {
 	      first->destroy();
@@ -890,14 +890,14 @@ namespace spot
 	  //   - (0 W Exp) = Exp
 	  //   - (1 W Exp) = 1
 	  //   - (Exp W Exp) = Exp
-	  if (second->is_true()
-	      || first->is_false()
+	  if (second->is_tt()
+	      || first->is_ff()
 	      || first == second)
 	    {
 	      first->destroy();
 	      return second;
 	    }
-	  if (first->is_true())
+	  if (first->is_tt())
 	    {
 	      second->destroy();
 	      return first;
@@ -908,9 +908,9 @@ namespace spot
 	  //   - (Exp R 0) = 0
 	  //   - (1 R Exp) = Exp
 	  //   - (Exp R Exp) = Exp
-	  if (second->is_true()
-	      || second->is_false()
-	      || first->is_true()
+	  if (second->is_tt()
+	      || second->is_ff()
+	      || first->is_tt()
 	      || first == second)
 	    {
 	      first->destroy();
@@ -922,14 +922,14 @@ namespace spot
 	  //   - (1 M Exp) = Exp
 	  //   - (0 M Exp) = 0
 	  //   - (Exp M Exp) = Exp
-	  if (second->is_false()
-	      || first->is_true()
+	  if (second->is_ff()
+	      || first->is_tt()
 	      || first == second)
 	    {
 	      first->destroy();
 	      return second;
 	    }
-	  if (first->is_false())
+	  if (first->is_ff())
 	    {
 	      second->destroy();
 	      return first;
@@ -942,15 +942,15 @@ namespace spot
 	  //   - [*0] <>-> Exp = 0
 	  //   - Exp <>-> 0 = 0
 	  //   - boolExp <>-> Exp = boolExp & Exp
-	  if (first->is_true())
+	  if (first->is_tt())
 	    return second;
-	  if (first->is_false()
+	  if (first->is_ff()
 	      || first->is_eword())
 	    {
 	      second->destroy();
 	      return ff();
 	    }
-	  if (second->is_false())
+	  if (second->is_ff())
 	    {
 	      first->destroy();
 	      return second;
@@ -964,15 +964,15 @@ namespace spot
 	  //   - [*0] []-> Exp = 1
 	  //   - Exp []-> 1 = 1
 	  //   - boolExp []-> Exp = !boolExp | Exp
-	  if (first->is_true())
+	  if (first->is_tt())
 	    return second;
-	  if (first->is_false()
+	  if (first->is_ff()
 	      || first->is_eword())
 	    {
 	      second->destroy();
 	      return tt();
 	    }
-	  if (second->is_true())
+	  if (second->is_tt())
 	    {
 	      first->destroy();
 	      return second;
@@ -1000,13 +1000,13 @@ namespace spot
       m.ap2name.emplace(next_id_, name);
       // next_id_ is incremented by setup_props(), called by the
       // constructor of fnode
-      return ires.first->second = new fnode(op::AP, {});
+      return ires.first->second = new fnode(op::ap, {});
     }
 
     const std::string&
     fnode::ap_name() const
     {
-      if (op_ != op::AP)
+      if (op_ != op::ap)
 	throw std::runtime_error("ap_name() called on non-AP formula");
       auto i = m.ap2name.find(id());
       assert(i != m.ap2name.end());
@@ -1014,9 +1014,9 @@ namespace spot
     }
 
     size_t fnode::next_id_ = 0U;
-    const fnode* fnode::ff_ = new fnode(op::False, {});
-    const fnode* fnode::tt_ = new fnode(op::True, {});
-    const fnode* fnode::ew_ = new fnode(op::EmptyWord, {});
+    const fnode* fnode::ff_ = new fnode(op::ff, {});
+    const fnode* fnode::tt_ = new fnode(op::tt, {});
+    const fnode* fnode::ew_ = new fnode(op::eword, {});
     const fnode* fnode::one_star_ = nullptr; // Only built when necessary.
 
     void fnode::setup_props(op o)
@@ -1032,8 +1032,8 @@ namespace spot
 
       switch (op_)
 	{
-	case op::False:
-	case op::True:
+	case op::ff:
+	case op::tt:
 	  is_.boolean = true;
 	  is_.sugar_free_boolean = true;
 	  is_.in_nenoform = true;
@@ -1055,7 +1055,7 @@ namespace spot
 	  is_.lbt_atomic_props = true;
 	  is_.spin_atomic_props = true;
 	  break;
-	case op::EmptyWord:
+	case op::eword:
 	  is_.boolean = false;
 	  is_.sugar_free_boolean = false;
 	  is_.in_nenoform = true;
@@ -1077,7 +1077,7 @@ namespace spot
 	  is_.lbt_atomic_props = true;
 	  is_.spin_atomic_props = true;
 	  break;
-	case op::AP:
+	case op::ap:
 	  is_.boolean = true;
 	  is_.sugar_free_boolean = true;
 	  is_.in_nenoform = true;
@@ -1119,7 +1119,7 @@ namespace spot
 	  is_.not_marked = true;
 	  is_.eventual = children[0]->is_universal();
 	  is_.universal = children[0]->is_eventual();
-	  is_.in_nenoform = (children[0]->is(op::AP));
+	  is_.in_nenoform = (children[0]->is(op::ap));
 	  is_.sere_formula = is_.boolean;
 
 	  is_.syntactic_safety = children[0]->is_syntactic_guarantee();
@@ -1336,7 +1336,7 @@ namespace spot
 	  is_.not_marked = true;
 	  // f U g is universal if g is eventual, or if f == 1.
 	  is_.eventual = children[1]->is_eventual();
-	  is_.eventual |= children[0]->is_true();
+	  is_.eventual |= children[0]->is_tt();
 	  is_.boolean = false;
 	  is_.sere_formula = false;
 	  is_.finite = false;
@@ -1357,7 +1357,7 @@ namespace spot
 	  props = children[0]->props & children[1]->props;
 	  is_.not_marked = true;
 	  // f W g is universal if f and g are, or if g == 0.
-	  is_.universal |= children[1]->is_false();
+	  is_.universal |= children[1]->is_ff();
 	  is_.boolean = false;
 	  is_.sere_formula = false;
 	  is_.finite = false;
@@ -1380,7 +1380,7 @@ namespace spot
 	  is_.not_marked = true;
 	  // g R f is universal if f is universal, or if g == 0.
 	  is_.universal = children[1]->is_universal();
-	  is_.universal |= children[0]->is_false();
+	  is_.universal |= children[0]->is_ff();
 	  is_.boolean = false;
 	  is_.sere_formula = false;
 	  is_.finite = false;
@@ -1402,7 +1402,7 @@ namespace spot
 	  props = children[0]->props & children[1]->props;
 	  is_.not_marked = true;
 	  // g M f is eventual if both g and f are eventual, or if f == 1.
-	  is_.eventual |= children[1]->is_true();
+	  is_.eventual |= children[1]->is_tt();
 	  is_.boolean = false;
 	  is_.sere_formula = false;
 	  is_.finite = false;
@@ -1585,7 +1585,7 @@ namespace spot
 	  if (m != unbounded())
 	    os << +m;
 	}
-      if (op_ == op::AP)
+      if (op_ == op::ap)
 	os << " \"" << ap_name() << '"';
       if (auto s = size())
 	{
diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh
index ba79ed952..dda416778 100644
--- a/src/ltlast/formula.hh
+++ b/src/ltlast/formula.hh
@@ -41,10 +41,10 @@ namespace spot
   {
     enum class op: uint8_t
     {
-      False,
-	True,
-	EmptyWord,
-	AP,
+      ff,
+	tt,
+	eword,
+	ap,
       // unary operators
 	Not,
 	X,
@@ -210,9 +210,9 @@ namespace spot
 	return ff_;
       }
 
-      bool is_false() const
+      bool is_ff() const
       {
-	return op_ == op::False;
+	return op_ == op::ff;
       }
 
       static const fnode* tt()
@@ -220,9 +220,9 @@ namespace spot
 	return tt_;
       }
 
-      bool is_true() const
+      bool is_tt() const
       {
-	return op_ == op::True;
+	return op_ == op::tt;
       }
 
       static const fnode* eword()
@@ -232,12 +232,12 @@ namespace spot
 
       bool is_eword() const
       {
-	return op_ == op::EmptyWord;
+	return op_ == op::eword;
       }
 
       bool is_constant() const
       {
-	return op_ == op::False || op_ == op::True || op_ == op::EmptyWord;
+	return op_ == op::ff || op_ == op::tt || op_ == op::eword;
       }
 
       bool is_Kleene_star() const
@@ -579,7 +579,7 @@ namespace spot
 		  {
 		    if (f->is(op::Not))
 		      f = f->nth(0);
-		    if (f->is(op::AP))
+		    if (f->is(op::ap))
 		      return f;
 		    return nullptr;
 		  };
@@ -1088,9 +1088,9 @@ namespace spot
 	return formula(fnode::ff());
       }
 
-      bool is_false() const
+      bool is_ff() const
       {
-	return ptr_->is_false();
+	return ptr_->is_ff();
       }
 
       static formula tt()
@@ -1098,9 +1098,9 @@ namespace spot
 	return formula(fnode::tt());
       }
 
-      bool is_true() const
+      bool is_tt() const
       {
-	return ptr_->is_true();
+	return ptr_->is_tt();
       }
 
       static formula eword()
@@ -1130,7 +1130,7 @@ namespace spot
 
       bool is_literal()
       {
-	return (is(op::AP) ||
+	return (is(op::ap) ||
 		// If f is in nenoform, Not can only occur in front of
 		// an atomic proposition.  So this way we do not have
 		// to check the type of the child.
@@ -1194,10 +1194,10 @@ namespace spot
       {
 	switch (op o = kind())
 	  {
-	  case op::False:
-	  case op::True:
-	  case op::EmptyWord:
-	  case op::AP:
+	  case op::ff:
+	  case op::tt:
+	  case op::eword:
+	  case op::ap:
 	    return *this;
 	  case op::Not:
 	  case op::X:
diff --git a/src/ltlvisit/apcollect.cc b/src/ltlvisit/apcollect.cc
index 1316172f6..9abd22578 100644
--- a/src/ltlvisit/apcollect.cc
+++ b/src/ltlvisit/apcollect.cc
@@ -47,7 +47,7 @@ namespace spot
 	s = new atomic_prop_set;
       f.traverse([&](const formula& f)
 		 {
-		   if (f.is(op::AP))
+		   if (f.is(op::ap))
 		     s->insert(f);
 		   return false;
 		 });
diff --git a/src/ltlvisit/dot.cc b/src/ltlvisit/dot.cc
index 1b5d12cb0..66531d916 100644
--- a/src/ltlvisit/dot.cc
+++ b/src/ltlvisit/dot.cc
@@ -60,9 +60,9 @@ namespace spot
 	    return src;
 
 	  op o = f.kind();
-	  std::string str = (o == op::AP) ? f.ap_name() : f.kindstr();
+	  std::string str = (o == op::ap) ? f.ap_name() : f.kindstr();
 
-	  if (o == op::AP || f.is_constant())
+	  if (o == op::ap || f.is_constant())
 	    *sinks_ << "    " << src << " [label=\""
 		    << str << "\", shape=box];\n";
 	  else
@@ -71,10 +71,10 @@ namespace spot
 	  int childnum = 0;
 	  switch (o)
 	    {
-	    case op::False:
-	    case op::True:
-	    case op::EmptyWord:
-	    case op::AP:
+	    case op::ff:
+	    case op::tt:
+	    case op::eword:
+	    case op::ap:
 	    case op::Not:
 	    case op::X:
 	    case op::F:
diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc
index 195eff603..b970d402d 100644
--- a/src/ltlvisit/mark.cc
+++ b/src/ltlvisit/mark.cc
@@ -37,10 +37,10 @@ namespace spot
       ltl::formula res;
       switch (f.kind())
 	{
-	case op::False:
-	case op::True:
-	case op::EmptyWord:
-	case op::AP:
+	case op::ff:
+	case op::tt:
+	case op::eword:
+	case op::ap:
 	case op::Not:
 	case op::X:
 	case op::F:
@@ -103,10 +103,10 @@ namespace spot
       ltl::formula res;
       switch (f.kind())
 	{
-	case op::False:
-	case op::True:
-	case op::EmptyWord:
-	case op::AP:
+	case op::ff:
+	case op::tt:
+	case op::eword:
+	case op::ap:
 	case op::Not:
 	case op::X:
 	case op::F:
diff --git a/src/ltlvisit/mutation.cc b/src/ltlvisit/mutation.cc
index 981d7544d..125406fda 100644
--- a/src/ltlvisit/mutation.cc
+++ b/src/ltlvisit/mutation.cc
@@ -67,11 +67,11 @@ namespace spot
 
 	  switch (f.kind())
 	    {
-	    case op::False:
-	    case op::True:
-	    case op::EmptyWord:
+	    case op::ff:
+	    case op::tt:
+	    case op::eword:
 	      return f;
-	    case op::AP:
+	    case op::ap:
 	      if (opts_ & Mut_Ap2Const)
 		{
 		  if (mutation_counter_-- == 0)
diff --git a/src/ltlvisit/print.cc b/src/ltlvisit/print.cc
index 84398fe4e..ca9aacacd 100644
--- a/src/ltlvisit/print.cc
+++ b/src/ltlvisit/print.cc
@@ -423,16 +423,16 @@ namespace spot
 	  op o = f.kind();
 	  switch (o)
 	    {
-	    case op::False:
+	    case op::ff:
 	      emit(KFalse);
 	      break;
-	    case op::True:
+	    case op::tt:
 	      emit(KTrue);
 	      break;
-	    case op::EmptyWord:
+	    case op::eword:
 	      emit(KEmptyWord);
 	      break;
-	    case op::AP:
+	    case op::ap:
 	      {
 		const std::string& str = f.ap_name();
 		if (!is_bare_word(str.c_str()))
@@ -483,7 +483,7 @@ namespace spot
 	    case op::Not:
 	      {
 		formula c = f[0];
-		if (c.is(op::AP))
+		if (c.is(op::ap))
 		  {
 		    // If we negate a single letter in UTF-8, use a
 		    // combining overline.
@@ -585,7 +585,7 @@ namespace spot
 		formula right = f[1];
 		unsigned last = left.size() - 1;
 		bool onelast = false;
-		if (left.is(op::Concat) && left[last].is_true())
+		if (left.is(op::Concat) && left[last].is_tt())
 		  {
 		    visit(left.all_but(last));
 		    onelast = true;
@@ -609,7 +609,7 @@ namespace spot
 		  }
 		else if (o == op::EConcat)
 		  {
-		    if (f[1].is(op::True))
+		    if (f[1].is_tt())
 		      {
 			os_ << '!';
 			// No recursion on right.
@@ -743,7 +743,7 @@ namespace spot
 		unsigned default_max = formula::unbounded();
 
 		// Abbreviate "1[*]" as "[*]".
-		if (!c.is(op::True) || o != op::Star)
+		if (!c.is_tt() || o != op::Star)
 		  {
 		    if (o == op::Star)
 		      {
@@ -1042,13 +1042,13 @@ namespace spot
 	  op o = f.kind();
 	  switch (o)
 	    {
-	    case op::False:
+	    case op::ff:
 	      os_ << 'f';
 	      break;
-	    case op::True:
+	    case op::tt:
 	      os_ << 't';
 	      break;
-	    case op::AP:
+	    case op::ap:
 	      {
 		const std::string& str = f.ap_name();
 		if (!is_pnum(str.c_str()))
@@ -1100,7 +1100,7 @@ namespace spot
 		os_ << "& ";
 	      first_ = true;
 	      break;
-	    case op::EmptyWord:
+	    case op::eword:
 	    case op::Closure:
 	    case op::NegClosure:
 	    case op::NegClosureMarked:
diff --git a/src/ltlvisit/relabel.cc b/src/ltlvisit/relabel.cc
index d715fc38c..f34c0cad4 100644
--- a/src/ltlvisit/relabel.cc
+++ b/src/ltlvisit/relabel.cc
@@ -121,7 +121,7 @@ namespace spot
 	formula
 	visit(formula f)
 	{
-	  if (f.is(op::AP))
+	  if (f.is(op::ap))
 	    return rename(f);
 	  else
 	    return f.map([this](formula f)
@@ -420,7 +420,7 @@ namespace spot
 	formula
 	visit(formula f)
 	{
-	  if (f.is(op::AP) || (c.find(f) != c.end()))
+	  if (f.is(op::ap) || (c.find(f) != c.end()))
 	    return rename(f);
 
 	  unsigned sz = f.size();
diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc
index d5a15bf64..9d5be9003 100644
--- a/src/ltlvisit/simpfg.cc
+++ b/src/ltlvisit/simpfg.cc
@@ -29,16 +29,16 @@ namespace spot
     formula simplify_f_g(formula p)
     {
       // 1 U p = Fp
-      if (p.is(op::U) && p[0].is_true())
+      if (p.is(op::U) && p[0].is_tt())
 	return formula::F(p[1]);
       // 0 R p = Gp
-      if (p.is(op::R) && p[0].is_false())
+      if (p.is(op::R) && p[0].is_ff())
 	return formula::G(p[1]);
       // p W 0 = Gp
-      if (p.is(op::W) && p[1].is_false())
+      if (p.is(op::W) && p[1].is_ff())
 	return formula::G(p[0]);
       // p M 1 = Fp
-      if (p.is(op::M) && p[1].is_true())
+      if (p.is(op::M) && p[1].is_tt())
 	return formula::F(p[0]);
       return p.map(simplify_f_g);
     }
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 479cd0004..9fdce4e2f 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -100,13 +100,13 @@ namespace spot
 
 	switch (f.kind())
 	  {
-	  case op::True:
+	  case op::tt:
 	    result = bddtrue;
 	    break;
-	  case op::False:
+	  case op::ff:
 	    result = bddfalse;
 	    break;
-	  case op::AP:
+	  case op::ap:
 	    result = bdd_ithvar(dict->register_proposition(f, this));
 	    break;
 	  case op::Not:
@@ -385,15 +385,15 @@ namespace spot
 
 	    switch (op o = f.kind())
 	      {
-	      case op::False:
-	      case op::True:
+	      case op::ff:
+	      case op::tt:
 		// Negation of constants is taken care of in the
 		// constructor of unop::Not, so these cases should be
 		// caught by nenoform_recursively().
 		assert(!negated);
 		result = f;
 		break;
-	      case op::AP:
+	      case op::ap:
 		result = negated ? formula::Not(f) : f;
 		break;
 	      case op::X:
@@ -526,7 +526,7 @@ namespace spot
 					  rec(f1, false), rec(f2, negated));
 		  break;
 		}
-	      case op::EmptyWord:
+	      case op::eword:
 	      case op::Not:
 		SPOT_UNREACHABLE();
 	      }
@@ -849,10 +849,10 @@ namespace spot
 
 	  switch (op o = f.kind())
 	    {
-	      case op::False:
-	      case op::True:
-	      case op::EmptyWord:
-	      case op::AP:
+	      case op::ff:
+	      case op::tt:
+	      case op::eword:
+	      case op::ap:
 	      case op::Not:
 	      case op::FStar:
 		return f;
@@ -1772,16 +1772,16 @@ namespace spot
 	  trace << "bo: trying basic reductions" << std::endl;
 	  // Rewrite U,R,W,M as F or G when possible.
 	  // true U b == F(b)
-	  if (bo.is(op::U) && a.is(op::True))
+	  if (bo.is(op::U) && a.is_tt())
 	    return recurse(formula::F(b));
 	  // false R b == G(b)
-	  if (bo.is(op::R) && a.is(op::False))
+	  if (bo.is(op::R) && a.is_ff())
 	    return recurse(formula::G(b));
 	  // a W false == G(a)
-	  if (bo.is(op::W) && b.is(op::False))
+	  if (bo.is(op::W) && b.is_ff())
 	    return recurse(formula::G(a));
 	  // a M true == F(a)
-	  if (bo.is(op::M) && b.is(op::True))
+	  if (bo.is(op::M) && b.is_tt())
 	    return recurse(formula::F(a));
 
 	  if (bo.is(op::W, op::M) || bo.is(op::U, op::R))
@@ -3292,9 +3292,9 @@ namespace spot
 
       if (f == g)
 	return true;
-      if (g.is(op::True) || f.is(op::False))
+      if (g.is_tt() || f.is_ff())
 	return true;
-      if (g.is(op::False) || f.is(op::True))
+      if (g.is_ff() || f.is_tt())
 	return false;
 
       // Often we compare a literal (an atomic_prop or its negation)
diff --git a/src/ltlvisit/snf.cc b/src/ltlvisit/snf.cc
index b563d9174..ff2f3a4ba 100644
--- a/src/ltlvisit/snf.cc
+++ b/src/ltlvisit/snf.cc
@@ -51,7 +51,7 @@ namespace spot
 	  formula out;
 	  switch (f.kind())
 	    {
-	    case op::EmptyWord:
+	    case op::eword:
 	      out = formula::ff();
 	      break;
 	    case op::Star:
@@ -95,9 +95,9 @@ namespace spot
 		out = formula::OrRat(v);
 		break;
 	      }
-	    case op::False:
-	    case op::True:
-	    case op::AP:
+	    case op::ff:
+	    case op::tt:
+	    case op::ap:
 	    case op::Not:
 	    case op::X:
 	    case op::F:
diff --git a/src/ltlvisit/unabbrev.cc b/src/ltlvisit/unabbrev.cc
index 51ad9a519..d24e93818 100644
--- a/src/ltlvisit/unabbrev.cc
+++ b/src/ltlvisit/unabbrev.cc
@@ -92,10 +92,10 @@ namespace spot
 
       switch (out.kind())
 	{
-	  case op::False:
-	  case op::True:
-	  case op::EmptyWord:
-	  case op::AP:
+	  case op::ff:
+	  case op::tt:
+	  case op::eword:
+	  case op::ap:
 	  case op::Not:
 	  case op::X:
 	  case op::Closure:
diff --git a/src/tests/parseerr.test b/src/tests/parseerr.test
index 46e132494..2c138a2bb 100755
--- a/src/tests/parseerr.test
+++ b/src/tests/parseerr.test
@@ -96,7 +96,7 @@ a & (, a & 0
 EOF
 run 0 ../equals -E recover.txt
 
-check 'a - b' 'AP(@3 #0 "a")' '>>> a - b
+check 'a - b' 'ap(@3 #0 "a")' '>>> a - b
       ^
 syntax error, unexpected $undefined
 
@@ -105,7 +105,7 @@ syntax error, unexpected $undefined
 ignoring trailing garbage
 '
 
-check '{a[*9999999999]}' 'Closure(@5 #0 [Star(@4 #0 0.. [AP(@3 #0 "a")])])' \
+check '{a[*9999999999]}' 'Closure(@5 #0 [Star(@4 #0 0.. [ap(@3 #0 "a")])])' \
 '>>> {a[*9999999999]}
         ^^^^^^^^^^
 value too large ignored
diff --git a/src/tests/utf8.test b/src/tests/utf8.test
index 6ccca4991..76ab3774c 100755
--- a/src/tests/utf8.test
+++ b/src/tests/utf8.test
@@ -26,12 +26,12 @@ set -e
 
 # ----
 run 0 ../ltl2text '□◯a' >out
-echo 'G(@5 #0 [X(@4 #0 [AP(@3 #0 "a")])])' > exp
+echo 'G(@5 #0 [X(@4 #0 [ap(@3 #0 "a")])])' > exp
 cmp out exp
 
 # ----
 run 0 ../ltl2text '□◯"αβγ"' >out
-echo 'G(@5 #0 [X(@4 #0 [AP(@3 #0 "αβγ")])])' > exp
+echo 'G(@5 #0 [X(@4 #0 [ap(@3 #0 "αβγ")])])' > exp
 cmp out exp
 
 
diff --git a/src/twa/acc.cc b/src/twa/acc.cc
index d3364e7e2..5a3bc8450 100644
--- a/src/twa/acc.cc
+++ b/src/twa/acc.cc
@@ -411,9 +411,9 @@ namespace spot
 
   int acc_cond::is_rabin() const
   {
-    if (code_.is_false())
+    if (code_.is_ff())
       return num_ == 0 ? 0 : -1;
-    if ((num_ & 1) || code_.is_true())
+    if ((num_ & 1) || code_.is_tt())
       return -1;
 
     if (is_rs(code_, acc_op::Or, acc_op::And, all_sets()))
@@ -424,9 +424,9 @@ namespace spot
 
   int acc_cond::is_streett() const
   {
-    if (code_.is_true())
+    if (code_.is_tt())
       return num_ == 0 ? 0 : -1;
-    if ((num_ & 1) || code_.is_false())
+    if ((num_ & 1) || code_.is_ff())
       return -1;
 
     if (is_rs(code_, acc_op::And, acc_op::Or, all_sets()))
@@ -444,7 +444,7 @@ namespace spot
 	pairs.resize(num_);
 	return true;
       }
-    if (code_.is_true()
+    if (code_.is_tt()
 	|| code_.back().op != acc_op::Or)
       return false;
 
@@ -670,7 +670,7 @@ namespace spot
     if (sets == 0)
       {
 	max = true;
-	odd = is_true();
+	odd = is_tt();
 	return true;
       }
     acc_cond::mark_t u_inf;
@@ -1107,7 +1107,7 @@ namespace spot
 
   acc_cond::acc_code acc_cond::acc_code::complement() const
   {
-    if (is_true())
+    if (is_tt())
       return acc_cond::acc_code::f();
     return complement_rec(&back());
   }
@@ -1169,7 +1169,7 @@ namespace spot
   acc_cond::acc_code
   acc_cond::acc_code::strip(acc_cond::mark_t rem, bool missing) const
   {
-    if (is_true() || is_false())
+    if (is_tt() || is_ff())
       return *this;
     return strip_rec(&back(), rem, missing);
   }
@@ -1177,7 +1177,7 @@ namespace spot
   acc_cond::mark_t
   acc_cond::acc_code::used_sets() const
   {
-    if (is_true() || is_false())
+    if (is_tt() || is_ff())
       return 0U;
     acc_cond::mark_t used_in_cond = 0U;
     auto pos = &back();
@@ -1205,7 +1205,7 @@ namespace spot
   std::pair<acc_cond::mark_t, acc_cond::mark_t>
   acc_cond::acc_code::used_inf_fin_sets() const
   {
-    if (is_true() || is_false())
+    if (is_tt() || is_ff())
       return {0U, 0U};
 
     acc_cond::mark_t used_fin = 0U;
diff --git a/src/twa/acc.hh b/src/twa/acc.hh
index 15165037e..dc5233862 100644
--- a/src/twa/acc.hh
+++ b/src/twa/acc.hh
@@ -395,14 +395,14 @@ namespace spot
 	return !(*this == other);
       }
 
-      bool is_true() const
+      bool is_tt() const
       {
 	unsigned s = size();
 	return s == 0
 	  || ((*this)[s - 1].op == acc_op::Inf && (*this)[s - 2].mark == 0U);
       }
 
-      bool is_false() const
+      bool is_ff() const
       {
 	unsigned s = size();
 	return s > 1
@@ -561,12 +561,12 @@ namespace spot
 
       void append_and(acc_code&& r)
       {
-	if (is_true() || r.is_false())
+	if (is_tt() || r.is_ff())
 	  {
 	    *this = std::move(r);
 	    return;
 	  }
-	if (is_false() || r.is_true())
+	if (is_ff() || r.is_tt())
 	  return;
 	unsigned s = size() - 1;
 	unsigned rs = r.size() - 1;
@@ -652,12 +652,12 @@ namespace spot
 
       void append_and(const acc_code& r)
       {
-	if (is_true() || r.is_false())
+	if (is_tt() || r.is_ff())
 	  {
 	    *this = r;
 	    return;
 	  }
-	if (is_false() || r.is_true())
+	if (is_ff() || r.is_tt())
 	  return;
 	unsigned s = size() - 1;
 	unsigned rs = r.size() - 1;
@@ -742,9 +742,9 @@ namespace spot
 
       void append_or(acc_code&& r)
       {
-	if (is_true() || r.is_false())
+	if (is_tt() || r.is_ff())
 	  return;
-	if (is_false() || r.is_true())
+	if (is_ff() || r.is_tt())
 	  {
 	    *this = std::move(r);
 	    return;
@@ -894,14 +894,14 @@ namespace spot
       return uses_fin_acceptance_;
     }
 
-    bool is_true() const
+    bool is_tt() const
     {
-      return code_.is_true();
+      return code_.is_tt();
     }
 
-    bool is_false() const
+    bool is_ff() const
     {
-      return code_.is_false();
+      return code_.is_ff();
     }
 
     bool is_buchi() const
diff --git a/src/twa/formula2bdd.cc b/src/twa/formula2bdd.cc
index 86fc439fe..85d89a933 100644
--- a/src/twa/formula2bdd.cc
+++ b/src/twa/formula2bdd.cc
@@ -72,11 +72,11 @@ namespace spot
       };
     switch (f.kind())
       {
-      case op::False:
+      case op::ff:
 	return bddfalse;
-      case op::True:
+      case op::tt:
 	return bddtrue;
-      case op::EmptyWord:
+      case op::eword:
       case op::Star:
       case op::FStar:
       case op::F:
@@ -98,7 +98,7 @@ namespace spot
       case op::OrRat:
       case op::AndRat:
 	SPOT_UNIMPLEMENTED();
-      case op::AP:
+      case op::ap:
 	return bdd_ithvar(d->register_proposition(f, owner));
       case op::Not:
 	return bdd_not(recurse(f[0]));
diff --git a/src/twaalgos/gtec/gtec.cc b/src/twaalgos/gtec/gtec.cc
index 04a53bd07..930d7997c 100644
--- a/src/twaalgos/gtec/gtec.cc
+++ b/src/twaalgos/gtec/gtec.cc
@@ -133,7 +133,7 @@ namespace spot
   {
     {
       auto acc = ecs_->aut->acc();
-      if (acc.get_acceptance().is_false())
+      if (acc.get_acceptance().is_ff())
 	return nullptr;
       if (acc.uses_fin_acceptance())
 	throw std::runtime_error
@@ -395,7 +395,7 @@ namespace spot
   {
     {
       auto acc = ecs_->aut->acc();
-      if (acc.get_acceptance().is_false())
+      if (acc.get_acceptance().is_ff())
 	return nullptr;
       if (acc.uses_fin_acceptance())
 	throw std::runtime_error
diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc
index 011c05424..0e266ca0b 100644
--- a/src/twaalgos/hoa.cc
+++ b/src/twaalgos/hoa.cc
@@ -299,7 +299,7 @@ namespace spot
     acc_cond::acc_code acc_c = aut->acc().get_acceptance();
     if (aut->acc().is_generalized_buchi())
       {
-	if (aut->acc().is_true())
+	if (aut->acc().is_tt())
 	  os << "acc-name: all";
 	else if (aut->acc().is_buchi())
 	  os << "acc-name: Buchi";
@@ -309,7 +309,7 @@ namespace spot
       }
     else if (aut->acc().is_generalized_co_buchi())
       {
-	if (aut->acc().is_false())
+	if (aut->acc().is_ff())
 	  os << "acc-name: none";
 	else if (aut->acc().is_co_buchi())
 	  os << "acc-name: co-Buchi";
diff --git a/src/twaalgos/ltl2taa.cc b/src/twaalgos/ltl2taa.cc
index 1285c66a2..5d1a9980c 100644
--- a/src/twaalgos/ltl2taa.cc
+++ b/src/twaalgos/ltl2taa.cc
@@ -60,9 +60,9 @@ namespace spot
 	init_ = f;
 	switch (f.kind())
 	  {
-	  case op::False:
+	  case op::ff:
 	    return;
-	  case op::True:
+	  case op::tt:
 	    {
 	      std::vector<formula> empty;
 	      res_->create_transition(init_, empty);
@@ -70,9 +70,9 @@ namespace spot
 	      succ_.push_back(ss);
 	      return;
 	    }
-	  case op::EmptyWord:
+	  case op::eword:
 	    SPOT_UNIMPLEMENTED();
-	  case op::AP:
+	  case op::ap:
 	    {
 	      if (negated_)
 		f = formula::Not(f);
diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc
index fbf706bdc..1a4130cbf 100644
--- a/src/twaalgos/ltl2tgba_fm.cc
+++ b/src/twaalgos/ltl2tgba_fm.cc
@@ -81,7 +81,7 @@ namespace spot
 	  else if (sub.is(op::W))
 	    {
 	      // f W 0 = Gf
-	      if (sub[1].is_false())
+	      if (sub[1].is_ff())
 		implied_subformulae(sub[0], rec, true);
 	    }
 	  else
@@ -90,7 +90,7 @@ namespace spot
 		// in 'f R g' and 'f M g' always evaluate 'g'.
 		formula b = sub;
 		sub = b[1];
-		if (b[0].is_false())
+		if (b[0].is_ff())
 		  {
 		    assert(b.is(op::R)); // because 0 M g = 0
 		    // 0 R f = Gf
@@ -539,7 +539,7 @@ namespace spot
 
       bdd now_to_concat()
       {
-	if (to_concat_ && !to_concat_.is(op::EmptyWord))
+	if (to_concat_ && !to_concat_.is(op::eword))
 	  return recurse(to_concat_);
 	return bddfalse;
       }
@@ -557,14 +557,14 @@ namespace spot
 	    bdd label = bdd_exist(cube, dict_.next_set);
 	    bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
 	    formula dest = dict_.conj_bdd_to_sere(dest_bdd);
-	    if (dest.is(op::EmptyWord))
+	    if (dest.is(op::eword))
 	      {
 		out |= label & next_to_concat();
 	      }
 	    else
 	      {
 		formula dest2 = formula::Concat({dest, to_concat_});
-		if (!dest2.is(op::False))
+		if (!dest2.is_ff())
 		  out |=
 		    label & bdd_ithvar(dict_.register_next_variable(dest2));
 	      }
@@ -576,13 +576,13 @@ namespace spot
       {
 	switch (op o = f.kind())
 	  {
-	  case op::False:
+	  case op::ff:
 	    return bddfalse;
-	  case op::True:
+	  case op::tt:
 	    return next_to_concat();
-	  case op::EmptyWord:
+	  case op::eword:
 	    return now_to_concat();
-	  case op::AP:
+	  case op::ap:
 	    return (bdd_ithvar(dict_.register_proposition(f))
 		    & next_to_concat());
 	  case op::F:
@@ -661,7 +661,7 @@ namespace spot
 			  bdd label = bdd_exist(cube, dict_.next_set);
 			  bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
 			  formula dest = dict_.conj_bdd_to_sere(dest_bdd);
-			  if (dest.is(op::EmptyWord))
+			  if (dest.is(op::eword))
 			    {
 			      res |= label &
 				bdd_ithvar(dict_.register_next_variable(f));
@@ -669,7 +669,7 @@ namespace spot
 			  else
 			    {
 			      formula dest2 = formula::Concat({dest, f});
-			      if (!dest2.is(op::False))
+			      if (!dest2.is_ff())
 				res |= label & bdd_ithvar
 				  (dict_.register_next_variable(dest2));
 			    }
@@ -711,10 +711,10 @@ namespace spot
 
 		      // If the destination is not 0 or [*0], it means it
 		      // can have successors.  Fusion the tail.
-		      if (!dest.is(op::False, op::EmptyWord))
+		      if (!dest.is(op::ff, op::eword))
 			{
 			  formula dest2 = formula::Fusion({dest, f});
-			  if (!dest2.is(op::False))
+			  if (!dest2.is_ff())
 			    res |= label &
 			      bdd_ithvar(dict_.register_next_variable(dest2));
 			}
@@ -858,12 +858,12 @@ namespace spot
 		  // If the destination is not 0 or [*0], it means it
 		  // can have successors.  Fusion the tail and append
 		  // anything to concatenate.
-		  if (!dest.is(op::False, op::EmptyWord))
+		  if (!dest.is(op::ff, op::eword))
 		    {
 		      formula dest2 = formula::Fusion({dest, tail});
 		      if (to_concat_)
 			dest2 = formula::Concat({dest2, to_concat_});
-		      if (!dest2.is(op::False))
+		      if (!dest2.is_ff())
 			res |= label
 			  & bdd_ithvar(dict_.register_next_variable(dest2));
 		    }
@@ -1117,13 +1117,13 @@ namespace spot
       {
 	switch (op o = node.kind())
 	  {
-	  case op::False:
+	  case op::ff:
 	    return bddfalse;
-	  case op::True:
+	  case op::tt:
 	    return bddtrue;
-	  case op::EmptyWord:
+	  case op::eword:
 	    SPOT_UNIMPLEMENTED();
-	  case op::AP:
+	  case op::ap:
 	    return bdd_ithvar(dict_.register_proposition(node));
 	  case op::F:
 	    {
@@ -1248,7 +1248,7 @@ namespace spot
 		  else
 		    {
 		      formula dest2 = formula::unop(o, dest);
-		      if (dest2.is_false())
+		      if (dest2.is_ff())
 			continue;
 		      res |=
 			label & bdd_ithvar(dict_.register_next_variable(dest2));
@@ -1290,7 +1290,7 @@ namespace spot
 		  if (!dest.accepts_eword())
 		    {
 		      formula dest2 = formula::unop(o, dest);
-		      if (dest2.is_false())
+		      if (dest2.is_ff())
 			continue;
 		      res |= label
 			& bdd_ithvar(dict_.register_next_variable(dest2));
@@ -1333,7 +1333,7 @@ namespace spot
 	      // r(f1 W f2) = r(f2) + r(f1)           if recurring
 	      //
 	      // also f1 W 0 = G(f1), so we can enable recurring on f1
-	      bdd f1 = recurse(node[0], node[1].is_false());
+	      bdd f1 = recurse(node[0], node[1].is_ff());
 	      bdd f2 = recurse(node[1]);
 	      if (!recurring_)
 		f1 &= bdd_ithvar(dict_.register_next_variable(node));
@@ -1346,7 +1346,7 @@ namespace spot
 	      // r(f2) is in factor, so we can propagate the recurring_ flag.
 	      // if f1=false, we can also turn it on (0 R f = Gf).
 	      bdd res = recurse(node[1],
-				recurring_ || node[0].is_false());
+				recurring_ || node[0].is_ff());
 	      // r(f1 R f2) = r(f2)(r(f1) + X(f1 R f2))  if not recurring
 	      // r(f1 R f2) = r(f2)                      if recurring
 	      if (recurring_ && !dict_.unambiguous)
@@ -1419,7 +1419,7 @@ namespace spot
 
 		      formula dest2 = formula::binop(o, dest, node[1]);
 		      bool unamb = dict_.unambiguous;
-		      if (!dest2.is(op::False))
+		      if (!dest2.is_ff())
 			{
 			  // If the rhs is Boolean, the
 			  // unambiguous code will produce a more
@@ -1456,14 +1456,14 @@ namespace spot
 		      bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
 		      formula dest = dict_.conj_bdd_to_sere(dest_bdd);
 
-		      if (dest.is(op::EmptyWord))
+		      if (dest.is(op::eword))
 			{
 			  res |= label & f2;
 			}
 		      else
 			{
 			  formula dest2 = formula::binop(o, dest, node[1]);
-			  if (!dest2.is(op::False))
+			  if (!dest2.is_ff())
 			    res |= label &
 			      bdd_ithvar(dict_.register_next_variable(dest2));
 			  if (dest.accepts_eword())
@@ -2080,7 +2080,7 @@ namespace spot
 		  {
 		    dest = simplifier->simplify(dest);
 		    // Ignore the arc if the destination reduces to false.
-		    if (dest.is_false())
+		    if (dest.is_ff())
 		      continue;
 		  }
 
@@ -2131,11 +2131,11 @@ namespace spot
 	//     f ----> 1
 	//
 	// because there is no point in looping on f if we can go to 1.
-	if (dests.front().dest.is_true())
+	if (dests.front().dest.is_tt())
 	  {
 	    dest_map::iterator i = dests.begin();
 	    bdd c = bddfalse;
-	    while (i != dests.end() && i->dest.is_true())
+	    while (i != dests.end() && i->dest.is_tt())
 	      c |= i++->cond;
 	    for (; i != dests.end(); ++i)
 	      i->cond -= c;
@@ -2158,7 +2158,7 @@ namespace spot
 		  // When translating LTL for an event-based logic
 		  // with unobservable events, the 1 state should
 		  // accept all events, even unobservable events.
-		  if (unobs && t.dest.is_true() && now.is_true())
+		  if (unobs && t.dest.is_tt() && now.is_tt())
 		    t.cond = all_events;
 
 		  // Will this be a new state?
diff --git a/src/twaalgos/neverclaim.cc b/src/twaalgos/neverclaim.cc
index a38d360f8..014632070 100644
--- a/src/twaalgos/neverclaim.cc
+++ b/src/twaalgos/neverclaim.cc
@@ -205,7 +205,7 @@ namespace spot
   print_never_claim(std::ostream& os, const const_twa_ptr& g,
 			const char* options)
   {
-    if (!(g->acc().is_buchi() || g->acc().is_true()))
+    if (!(g->acc().is_buchi() || g->acc().is_tt()))
       throw std::runtime_error
 	("Never claim output only supports Büchi acceptance");
     never_claim_output d(os, options);
diff --git a/src/twaalgos/product.cc b/src/twaalgos/product.cc
index 6ac27c8fc..158e4cb0d 100644
--- a/src/twaalgos/product.cc
+++ b/src/twaalgos/product.cc
@@ -81,7 +81,7 @@ namespace spot
 	};
 
       res->set_init_state(new_state(left_state, right_state));
-      if (right_acc.is_false())
+      if (right_acc.is_ff())
 	// Do not bother doing any work if the resulting acceptance is
 	// false.
 	return res;
diff --git a/src/twaalgos/remfin.cc b/src/twaalgos/remfin.cc
index d51d9f14b..bfe284e3d 100644
--- a/src/twaalgos/remfin.cc
+++ b/src/twaalgos/remfin.cc
@@ -311,7 +311,7 @@ namespace spot
 
       auto code = aut->get_acceptance();
 
-      if (code.is_true())
+      if (code.is_tt())
 	return nullptr;
 
       acc_cond::mark_t inf_pairs = 0U;
@@ -586,7 +586,7 @@ namespace spot
 	  auto c = acc.inf(m);
 	  for (unsigned i = 0; i < sz; ++i)
 	    {
-	      if (!code[i].is_true())
+	      if (!code[i].is_tt())
 		continue;
 	      add[i] = m;
 	      code[i].append_and(c);
diff --git a/src/twaalgos/safety.cc b/src/twaalgos/safety.cc
index c2b5677c4..3ee1b020b 100644
--- a/src/twaalgos/safety.cc
+++ b/src/twaalgos/safety.cc
@@ -65,7 +65,7 @@ namespace spot
 
   bool is_safety_mwdba(const const_twa_graph_ptr& aut)
   {
-    if (!(aut->acc().is_buchi() || aut->acc().is_true()))
+    if (!(aut->acc().is_buchi() || aut->acc().is_tt()))
       throw std::runtime_error
 	("is_safety_mwdba() should be called on a Buchi automaton");
 
diff --git a/wrap/python/spot.py b/wrap/python/spot.py
index d74257890..17177ebe4 100644
--- a/wrap/python/spot.py
+++ b/wrap/python/spot.py
@@ -124,7 +124,7 @@ def _formula_traverse(self, func):
 
 def _formula_map(self, func):
     k = self.kind()
-    if k in (FalseVal, TrueVal, EmptyWord, AP):
+    if k in (ff, tt, eword, ap):
         return self;
     if k in (Not, X, F, G, Closure, NegClosure, NegClosureMarked):
         return formula.unop(k, func(self[0]))