diff --git a/Kernel/HOL/BetaNormaliser.hpp b/Kernel/HOL/BetaNormaliser.hpp
index 90b486ed7..b7f0e0962 100644
--- a/Kernel/HOL/BetaNormaliser.hpp
+++ b/Kernel/HOL/BetaNormaliser.hpp
@@ -26,7 +26,7 @@ using namespace Kernel;
 class BetaNormaliser : public TermTransformer {
   unsigned reductions = 0;
 public:
-  BetaNormaliser() : TermTransformer(false) {}
+  BetaNormaliser() : TermTransformer(/*transformSorts=*/false) {}
 
   unsigned getReductions() const {
     return reductions;
diff --git a/Kernel/HOL/Convert.cpp b/Kernel/HOL/Convert.cpp
index 0f4d32f42..ec9f4a580 100644
--- a/Kernel/HOL/Convert.cpp
+++ b/Kernel/HOL/Convert.cpp
@@ -20,12 +20,6 @@
 using IndexSortPair = std::pair<int, TermList>;
 using VarToIndexMap = std::unordered_map<unsigned, IndexSortPair>;
 
-static TermList sortOf(TermList t) {
-  ASS(t.isTerm())
-
-  return SortHelper::getResultSort(t.term());
-}
-
 static TermList termToNameless(TermList term, const VarToIndexMap& map);
 static TermList formulaToNameless(Formula *formula, const VarToIndexMap& map);
 
@@ -40,7 +34,7 @@ static TermList toNamelessAux(VList* vars, SList* sorts, TermList body, TermList
     vars->tail() == nullptr ? termToNameless(body, newMap)
                             : toNamelessAux(vars->tail(), sorts->tail(), body, bodySort, newMap);
 
-  bodySort = converted.isVar() ? bodySort : sortOf(converted);
+  bodySort = converted.isVar() ? bodySort : converted.resultSort();
   return HOL::create::namelessLambda(sorts->head(), bodySort, converted);
 }
 
@@ -68,7 +62,7 @@ static TermList termToNameless(TermList term, const VarToIndexMap& map) {
         const auto vars = sd->getLambdaVars();
 
         const auto eliminated = toNamelessAux(vars, sorts, sd->getLambdaExp(), sd->getLambdaExpSort(), map);
-        ASS_REP2(eliminated.isVar() || sortOf(eliminated) == sd->getSort(), t->toString(), eliminated.toString())
+        ASS_REP2(eliminated.isVar() || eliminated.resultSort() == sd->getSort(), t->toString(), eliminated.toString())
         return eliminated;
       }
 
diff --git a/Kernel/HOL/Create.cpp b/Kernel/HOL/Create.cpp
index 7be33b0d3..a201abdc2 100644
--- a/Kernel/HOL/Create.cpp
+++ b/Kernel/HOL/Create.cpp
@@ -62,6 +62,36 @@ TermList HOL::create::app(TermList head, const TermStack& terms) {
   return app(SortHelper::getResultSort(head.term()), head, terms);
 }
 
+TermList HOL::create::equality(TermList sort) {
+  static const auto eqProxy = env.signature->getEqualityProxy();
+
+  return TermList(Term::create1(eqProxy, sort));
+}
+
+TermList HOL::create::neg() {
+  static const auto term = TermList(Term::createConstant(env.signature->getNotProxy()));
+
+  return term;
+}
+
+TermList HOL::create::pi(TermList sort) {
+  static const auto piProxy = env.signature->getPiSigmaProxy("vPI");
+
+  return TermList(Term::create1(piProxy, sort));
+}
+
+TermList HOL::create::sigma(TermList sort) {
+  static const auto sigmaProxy = env.signature->getPiSigmaProxy("vSIGMA");
+
+  return TermList(Term::create1(sigmaProxy, sort));
+}
+
+TermList HOL::create::placeholder(TermList sort) {
+  static const auto placeholder = env.signature->getPlaceholder();
+
+  return TermList(Term::create1(placeholder, sort));
+}
+
 Term* HOL::create::lambda(unsigned numArgs, const unsigned* vars, const TermList* varSorts, TypedTermList body, TermList* resultExprSort) {
   auto s = new (0, sizeof(Term::SpecialTermData)) Term;
   s->makeSymbol(Term::toNormalFunctor(SpecialFunctor::LAMBDA), 0);
diff --git a/Kernel/HOL/HOL.cpp b/Kernel/HOL/HOL.cpp
index f9ce3f66f..c0a2a0a20 100644
--- a/Kernel/HOL/HOL.cpp
+++ b/Kernel/HOL/HOL.cpp
@@ -13,6 +13,7 @@
 
 #include "Kernel/HOL/HOL.hpp"
 
+#include "ToPlaceholders.hpp"
 #include "Kernel/Formula.hpp"
 
 using IndexVarStack = Stack<std::pair<unsigned, unsigned>>;
@@ -123,6 +124,10 @@ static std::string toStringAux(const Term& term, bool topLevel, IndexVarStack& s
     return res;
   }
 
+  if (term.isPlaceholder()) {
+    return term.functionName() + "⟨" + term.nthArgument(0)->toString(true) + "⟩";
+  }
+
   if (term.isLambdaTerm()) {
     unsigned v = st.size() ? st.top().second + 1 : 0;
     std::string bvar = (pretty ? "y" : "Y") + Int::toString(v);
@@ -371,4 +376,4 @@ void HOL::getMatrixAndPrefSorts(TermList t, TermList& matrix, TermStack& sorts)
     t = t.lambdaBody();
   }
   matrix = t;
-}
\ No newline at end of file
+}
diff --git a/Kernel/HOL/HOL.hpp b/Kernel/HOL/HOL.hpp
index 240262064..808753bab 100644
--- a/Kernel/HOL/HOL.hpp
+++ b/Kernel/HOL/HOL.hpp
@@ -18,6 +18,8 @@
 #include "Kernel/TypedTermList.hpp"
 #include "Lib/Environment.hpp"
 
+#include <optional>
+
 /**
  * This namespace contains several helper functions to deal with higher-order terms.
  */
@@ -68,7 +70,7 @@ namespace HOL::create {
   TermList app(TermList sort, TermList head, TermList arg);
   TermList app(TermList head, TermList arg);
   TermList app(TermList s1, TermList s2, TermList arg1, TermList arg2, bool shared = true);
-  TermList app(TermList sort, TermList head, const TermStack& terms); // todo const termstack
+  TermList app(TermList sort, TermList head, const TermStack& terms);
   TermList app(TermList head, const TermStack& terms);
 
   inline TermList app2(TermList sort, TermList head, TermList arg1, TermList arg2) {
@@ -78,13 +80,14 @@ namespace HOL::create {
   inline TermList app2(TermList head, TermList arg1, TermList arg2) {
     ASS(head.isTerm())
 
-    return app2(Kernel::SortHelper::getResultSort(head.term()), head, arg1, arg2);
+    return app2(head.resultSort(), head, arg1, arg2);
   }
 
-  inline TermList equality(TermList sort) { return TermList(Term::create1(env.signature->getEqualityProxy(), sort)); }
-  inline TermList neg() { return TermList(Term::createConstant(env.signature->getNotProxy())); }
-  inline TermList pi(TermList sort) { return TermList(Term::create1(env.signature->getPiSigmaProxy("vPI"), sort)); }
-  inline TermList sigma(TermList sort) { return TermList(Term::create1(env.signature->getPiSigmaProxy("vSIGMA"), sort)); }
+  TermList equality(TermList sort);
+  TermList neg();
+  TermList pi(TermList sort);
+  TermList sigma(TermList sort);
+  TermList placeholder(TermList sort);
 
   Term* lambda(unsigned numArgs, const unsigned* vars, const TermList* varSorts, TypedTermList body, TermList* resultExprSort = nullptr);
 
@@ -93,6 +96,8 @@ namespace HOL::create {
 
   TermList surroundWithLambdas(TermList t, TermStack& sorts, bool fromTop = false);
   TermList surroundWithLambdas(TermList t, TermStack& sorts, TermList sort, bool fromTop = false);
+
+  TermList placeholder(TermList sort);
 } // namespace HOL::create
 
 namespace HOL::convert {
diff --git a/Kernel/HOL/RedexReducer.hpp b/Kernel/HOL/RedexReducer.hpp
index 86a91ca9d..669bd23db 100644
--- a/Kernel/HOL/RedexReducer.hpp
+++ b/Kernel/HOL/RedexReducer.hpp
@@ -20,7 +20,7 @@ using namespace Kernel;
 
 class RedexReducer : public TermTransformer {
 public:
-  RedexReducer() : TermTransformer(false) {}
+  RedexReducer() : TermTransformer(/*transformSorts=*/false) {}
 
   TermList reduce(TermList head, TermStack& args);
   TermList transformSubterm(TermList t) override;
diff --git a/Kernel/HOL/SubtermReplacer.cpp b/Kernel/HOL/SubtermReplacer.cpp
index 500613cd7..d9399d710 100644
--- a/Kernel/HOL/SubtermReplacer.cpp
+++ b/Kernel/HOL/SubtermReplacer.cpp
@@ -16,7 +16,7 @@
 #include "TermShifter.hpp"
 
 SubtermReplacer::SubtermReplacer(TermList what, TermList by, bool liftFree)
-      : TermTransformer(false),
+      : TermTransformer(/*transformSorts=*/false),
         _what(what),
         _by(by),
         _liftFreeIndices(liftFree) {
diff --git a/Kernel/HOL/SubtermReplacer.hpp b/Kernel/HOL/SubtermReplacer.hpp
index 2798aaa44..10e185fbf 100644
--- a/Kernel/HOL/SubtermReplacer.hpp
+++ b/Kernel/HOL/SubtermReplacer.hpp
@@ -24,7 +24,7 @@ using namespace Kernel;
  * In contrast to EqHelper::replace free de Bruijn indices of the new subterm can be automatically
  * lifted in order to avoid name capture.
  *
- * See also tSubtermReplacer.cpp for accompanying unit tests of this class.
+ * See also tHOL_SubtermReplacer.cpp for accompanying unit tests of this class.
  */
 class SubtermReplacer : public TermTransformer {
 public:
diff --git a/Kernel/HOL/TermShifter.hpp b/Kernel/HOL/TermShifter.hpp
index 8607ceb1a..627c58c35 100644
--- a/Kernel/HOL/TermShifter.hpp
+++ b/Kernel/HOL/TermShifter.hpp
@@ -31,13 +31,13 @@ using namespace Kernel;
  * Example:
  * TermTransformer::shift(t, 2) ~> { "(λ. f db_0) db_2", Option<unsigned>(0) }
  *
- * See also tTermShifter.cpp for accompanying unit tests of this class.
+ * See also tHOL_TermShifter.cpp for accompanying unit tests of this class.
  */
 class TermShifter : public TermTransformer
 {
 public:
   explicit TermShifter(int shiftBy)
-    : TermTransformer(false),
+    : TermTransformer(/*transformSorts=*/false),
       _shiftBy(shiftBy) {}
 
   // positive value -> shift up
diff --git a/Kernel/HOL/ToPlaceholders.cpp b/Kernel/HOL/ToPlaceholders.cpp
new file mode 100644
index 000000000..592c7fbb8
--- /dev/null
+++ b/Kernel/HOL/ToPlaceholders.cpp
@@ -0,0 +1,50 @@
+/*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+/**
+ * @file ToPlaceholders.cpp
+ */
+
+#include "Kernel/HOL/ToPlaceholders.hpp"
+#include "Kernel/HOL/HOL.hpp"
+
+ToPlaceholders::ToPlaceholders(Options::FunctionExtensionality funcExtMode)
+      : TermTransformer(/*transformSorts=*/false),
+        _nextIsPrefix(false),
+        _topLevel(true),
+        _mode(funcExtMode) {}
+
+TermList ToPlaceholders::replace(TermList term, std::optional<Options::FunctionExtensionality> funcExtMode) {
+  auto toPlaceholders = ToPlaceholders(funcExtMode.value_or(env.options->functionExtensionality()));
+
+  if (auto transformed = toPlaceholders.transformSubterm(term); transformed != term)
+    return transformed;
+
+  toPlaceholders._topLevel = false;
+  return toPlaceholders.transform(term);
+}
+
+TermList ToPlaceholders::transformSubterm(TermList t) {
+  if (_nextIsPrefix || t.isVar())
+    return t;
+
+  // Not expecting any unreduced redexes here
+  ASS(!t.head().isLambdaTerm())
+
+  auto sort = SortHelper::getResultSort(t.term());
+  if (t.isLambdaTerm() || t.head().isVar())
+    return HOL::create::placeholder(sort);
+
+  if (_mode == Options::FunctionExtensionality::ABSTRACTION) {
+    if (sort.isArrowSort() || sort.isVar() || (sort.isBoolSort() && !_topLevel)) {
+      return HOL::create::placeholder(sort);
+    }
+  }
+  return t;
+}
diff --git a/Kernel/HOL/ToPlaceholders.hpp b/Kernel/HOL/ToPlaceholders.hpp
new file mode 100644
index 000000000..eb6f06ba3
--- /dev/null
+++ b/Kernel/HOL/ToPlaceholders.hpp
@@ -0,0 +1,55 @@
+/*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+/**
+ * @file ToPlaceholders.hpp
+ */
+
+#ifndef __ToPlaceholders__
+#define __ToPlaceholders__
+
+
+#include "Kernel/TermTransformer.hpp"
+#include "Shell/Options.hpp"
+
+#include <optional>
+
+using namespace Kernel;
+
+/**
+* Replaces higher-order subterms (subterms with variable heads e.g., X a b and
+* lambda terms) with a special polymorphic constant we call a "placeholder".
+*
+* If the value of the FunctionExtensionality option is ABSTRACTION, functional and Boolean subterms are also be replaced
+*
+* See also tHOL_ToPlaceholders.cpp for accompanying unit tests of this class.
+*/
+class ToPlaceholders : public TermTransformer
+{
+public:
+  static TermList replace(TermList term, std::optional<Shell::Options::FunctionExtensionality> funcExtMode = std::nullopt);
+  TermList transformSubterm(TermList t) override;
+
+  void onTermEntry(Term* t) override {
+    if (t->isApplication())
+      _nextIsPrefix = true;
+  }
+
+  void onTermExit(Term* t) override {
+    _nextIsPrefix = false;
+  }
+
+private:
+  explicit ToPlaceholders(Shell::Options::FunctionExtensionality funcExtMode);
+  bool _nextIsPrefix;
+  bool _topLevel;
+  Shell::Options::FunctionExtensionality _mode;
+};
+
+#endif // __ToPlaceholders__
diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp
index a23e966a8..570cbde6a 100644
--- a/Kernel/Signature.cpp
+++ b/Kernel/Signature.cpp
@@ -583,7 +583,7 @@ unsigned Signature::getDiff() {
     auto alpha = TermList(0, false);
     auto beta = TermList(1, false);
     auto alphaBeta = AtomicSort::arrowSort(alpha, beta);
-    auto result = AtomicSort::arrowSort(alphaBeta, alphaBeta, alpha);
+    auto result = AtomicSort::arrowSort({alphaBeta, alphaBeta, alpha});
     auto sym = getFunction(diff);
     sym->setType(OperatorType::getConstantsType(result, 2));
   }
@@ -654,12 +654,13 @@ unsigned Signature::getChoice() {
 }
 
 unsigned Signature::getDeBruijnIndex(int index) {
+  ASS(index >= 0)
+
   bool added = false;
   unsigned fun = addFunction("db" + Int::toString(index), 1, added);
   if (added) {
-    auto alpha = TermList(0, false);
     auto sym = getFunction(fun);
-    sym->setType(OperatorType::getConstantsType(alpha, 1));
+    sym->setType(OperatorType::getConstantsType(TermList::var(0), 1));
     sym->setDeBruijnIndex(index);
   }
   return fun;
@@ -669,11 +670,9 @@ unsigned Signature::getPlaceholder() {
   if (_placeholderFun != UINT_MAX)
     return _placeholderFun;
 
-  unsigned fun = addFreshFunction(1,"ph");
+  unsigned fun = addFreshFunction(1, "ph");
   _placeholderFun = fun;
-  auto alpha = TermList(0, false);
-  auto sym = getFunction(fun);
-  sym->setType(OperatorType::getConstantsType(alpha, 1));
+  getFunction(fun)->setType(OperatorType::getConstantsType(TermList::var(0), 1));
   return fun;
 }
 
diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp
index 66c67f4a7..264c491a9 100644
--- a/Kernel/Signature.hpp
+++ b/Kernel/Signature.hpp
@@ -915,7 +915,7 @@ class Signature
     unsigned eqProxy = addFunction("vEQ",1, added);
     if(added){
       TermList tv = TermList(0, false);
-      TermList result = AtomicSort::arrowSort(tv, tv, AtomicSort::boolSort());
+      TermList result = AtomicSort::arrowSort({tv, tv, AtomicSort::boolSort()});
       Symbol * sym = getFunction(eqProxy);
       sym->setType(OperatorType::getConstantsType(result, 1));
       sym->setProxy(Proxy::EQUALS);
@@ -938,7 +938,7 @@ class Signature
     unsigned proxy = addFunction(name, 0, added);
     if (added) {
       auto bs = AtomicSort::boolSort();
-      auto result = AtomicSort::arrowSort(bs, bs, bs);
+      auto result = AtomicSort::arrowSort({bs, bs, bs});
       auto sym = getFunction(proxy);
       sym->setType(OperatorType::getConstantsType(result));
       sym->setProxy(convert(name));
diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp
index 9f503a217..75640dc01 100644
--- a/Kernel/Term.cpp
+++ b/Kernel/Term.cpp
@@ -143,6 +143,10 @@ bool TermList::isChoice() const {
   return !isVar() && term()->isChoice();
 }
 
+bool TermList::isPlaceholder() const {
+  return !isVar() && term()->isPlaceholder();
+}
+
 Option<unsigned> TermList::deBruijnIndex() const {
   if (isVar())
     return {};
@@ -182,24 +186,28 @@ TermList TermList::head() const {
   return trm;
 }
 
-std::pair<TermList, TermList> TermList::asPair() {
+std::pair<TermList, TermList> TermList::asPair() const {
   ASS(isArrowSort())
 
   return {domain(), result()};
 }
 
-TermList TermList::domain() {
+TermList TermList::domain() const {
   ASS(isArrowSort())
 
   return *term()->nthArgument(0);
 }
 
-TermList TermList::result() {
+TermList TermList::result() const {
   ASS(isArrowSort())
 
   return *term()->nthArgument(1);
 }
 
+TermList TermList::resultSort() const {
+  return SortHelper::getResultSort(term());
+}
+
 TermList TermList::replaceSubterm(TermList what, TermList by, bool liftFreeIndices) const {
   return SubtermReplacer(what, by, liftFreeIndices).replace(*this);
 }
@@ -306,28 +314,24 @@ unsigned TermList::weight() const
   return isVar() ? 1 : term()->weight();
 }
 
-bool TermList::isArrowSort()
-{
+bool TermList::isArrowSort() const {
   return !isVar() && term()->isSort() &&
-         static_cast<AtomicSort*>(term())->isArrowSort();
+         static_cast<const AtomicSort*>(term())->isArrowSort();
 }
 
-bool TermList::isBoolSort()
-{
+bool TermList::isBoolSort() const {
   return !isVar() && term()->isSort() &&
-         static_cast<AtomicSort*>(term())->isBoolSort();
+         static_cast<const AtomicSort*>(term())->isBoolSort();
 }
 
-bool TermList::isArraySort()
-{
+bool TermList::isArraySort() const {
   return !isVar() && term()->isSort() &&
-         static_cast<AtomicSort*>(term())->isArraySort();
+         static_cast<const AtomicSort*>(term())->isArraySort();
 }
 
-bool TermList::isTupleSort()
-{
+bool TermList::isTupleSort() const {
   return !isVar() && term()->isSort() &&
-         static_cast<AtomicSort*>(term())->isTupleSort();
+         static_cast<const AtomicSort*>(term())->isTupleSort();
 }
 
 bool AtomicSort::isArrowSort() const {
@@ -941,6 +945,10 @@ bool Term::isChoice() const {
   return !isSort() && !isLiteral() && !isSpecial() && env.signature->isChoiceFun(_functor);
 }
 
+bool Term::isPlaceholder() const {
+  return !isSort() && !isLiteral() && !isSpecial() && env.signature->isPlaceholder(_functor);
+}
+
 Option<unsigned> Term::deBruijnIndex() const {
   if (isSort() || isLiteral() || isSpecial())
     return {};
@@ -1305,10 +1313,6 @@ TermList AtomicSort::arrowSort(TermList s1, TermList s2) {
   return TermList(create2(arrow, s1, s2));
 }
 
-TermList AtomicSort::arrowSort(TermList s1, TermList s2, TermList s3) {
-  return arrowSort(s1, arrowSort(s2, s3));
-}
-
 TermList AtomicSort::arrowSort(unsigned size, const TermList* types, TermList range) {
   ASS(size > 0)
 
@@ -1319,6 +1323,14 @@ TermList AtomicSort::arrowSort(unsigned size, const TermList* types, TermList ra
   return res;
 }
 
+TermList AtomicSort::arrowSort(const std::initializer_list<TermList>& types) {
+  const auto size = types.size();
+  ASS(size >= 2)
+
+  const TermList* data = std::data(types);
+  return arrowSort(size - 1, data, data[size - 1]);
+}
+
 TermList AtomicSort::arrowSort(const TermStack & domSorts, TermList range) {
   TermList res = range;
   for (auto domSort : domSorts)
diff --git a/Kernel/Term.hpp b/Kernel/Term.hpp
index 052fea53d..9428802e0 100644
--- a/Kernel/Term.hpp
+++ b/Kernel/Term.hpp
@@ -274,10 +274,10 @@ class TermList {
   /** if not var, the inner term must be shared */
   unsigned weight() const;
   /** returns true if this termList is wrapping a higher-order "arrow" sort */
-  bool isArrowSort();
-  bool isBoolSort();
-  bool isArraySort();
-  bool isTupleSort();
+  bool isArrowSort() const;
+  bool isBoolSort() const;
+  bool isArraySort() const;
+  bool isTupleSort() const;
   bool containsSubterm(TermList v) const;
   bool containsAllVariablesOf(TermList t) const;
   bool ground() const;
@@ -289,15 +289,17 @@ class TermList {
   bool isRedex() const;
   bool isProxy(Proxy proxy) const;
   bool isChoice() const;
+  bool isPlaceholder() const;
 
   Option<unsigned> deBruijnIndex() const;
   TermList lhs() const;
   TermList rhs() const;
   TermList lambdaBody() const;
   TermList head() const;
-  std::pair<TermList, TermList> asPair();
-  TermList domain();
-  TermList result();
+  std::pair<TermList, TermList> asPair() const;
+  TermList domain() const;
+  TermList result() const;
+  TermList resultSort() const;
   TermList replaceSubterm(TermList what, TermList by, bool liftFreeIndices = false) const;
   /* End higher-order terms */
 
@@ -786,6 +788,7 @@ class alignas(8) Term
   bool isRedex() const;
   bool isProxy(Proxy proxy) const;
   bool isChoice() const;
+  bool isPlaceholder() const;
 
   TermList lambdaBody() const {
     ASS(isLambdaTerm())
@@ -1049,8 +1052,8 @@ class AtomicSort
   
   static TermList arrowSort(const TermStack& domSorts, TermList range);
   static TermList arrowSort(TermList s1, TermList s2);
-  static TermList arrowSort(TermList s1, TermList s2, TermList s3);
   static TermList arrowSort(unsigned size, const TermList* types, TermList range);
+  static TermList arrowSort(const std::initializer_list<TermList>& types);
   static TermList arraySort(TermList indexSort, TermList innerSort);
   static TermList tupleSort(unsigned arity, TermList* sorts);
   static TermList defaultSort();
diff --git a/Test/HOLUtils.cpp b/Test/HOLUtils.cpp
index 89518d68f..90fc1a858 100644
--- a/Test/HOLUtils.cpp
+++ b/Test/HOLUtils.cpp
@@ -44,30 +44,6 @@ TypedTermList lam(std::initializer_list<TypedTermList> typedVars, TypedTermList
   return {TermList(term), sort};
 }
 
-TypedTermList app(TypedTermList lhs, TypedTermList rhs) {
-  ASS(lhs.sort().isArrowSort())
-
-  auto [domain, result] = lhs.sort().asPair();
-
-  ASS(domain == rhs.sort())
-
-  return {::HOL::create::app(domain, result, lhs, rhs), result};
-}
-
-TypedTermList app(const std::initializer_list<TypedTermList>& terms) {
-  const auto size = terms.size();
-
-  ASS(size > 0)
-  auto a = std::data(terms);
-  TypedTermList res = a[0];
-
-  for (std::size_t i = 0; i + 1 < size; ++i) {
-    res = app(res, a[i+1]);
-  }
-
-  return res;
-}
-
 static TermList mkAtomicSort(const std::string& name) {
   return TermList(AtomicSort::createConstant(name));
 }
@@ -83,9 +59,10 @@ Defs::Defs() {
   fSrt = TermList(AtomicSort::arrowSort(srt, srt));
   a = mkConst("a", srt);
   f = mkConst("f", fSrt);
-  f2 = mkConst("f2", AtomicSort::arrowSort(srt, AtomicSort::arrowSort(srt, srt)));
-  f3 = mkConst("f3", AtomicSort::arrowSort(srt, AtomicSort::arrowSort(srt, AtomicSort::arrowSort(srt, srt))));
-  g = mkConst("g", AtomicSort::arrowSort(AtomicSort::arrowSort(srt, srt), srt));
+  f2 = mkConst("f2", AtomicSort::arrowSort({srt, srt, srt}));
+  f3 = mkConst("f3", AtomicSort::arrowSort({srt, srt, srt, srt}));
+  g = mkConst("g", AtomicSort::arrowSort(fSrt, srt));
+  h = mkConst("h", AtomicSort::arrowSort({fSrt, srt, srt}));
 }
 
 Defs* Defs::_instance = nullptr;
diff --git a/Test/HOLUtils.hpp b/Test/HOLUtils.hpp
index c5cd0aa4f..4d55fd6c4 100644
--- a/Test/HOLUtils.hpp
+++ b/Test/HOLUtils.hpp
@@ -16,6 +16,7 @@
 
 #include "Kernel/Term.hpp"
 #include "Kernel/TypedTermList.hpp"
+#include "Kernel/HOL/HOL.hpp"
 #include "Shell/Options.hpp"
 
 #include <optional>
@@ -41,8 +42,21 @@ inline TypedTermList lam(TypedTermList var, TypedTermList body) {
   return lam({var}, body);
 }
 
-TypedTermList app(TypedTermList lhs, TypedTermList rhs);
-TypedTermList app(const std::initializer_list<TypedTermList>& terms);
+template <class T, class ...Ts>
+TypedTermList app(TypedTermList arg1, T arg2, Ts... args) {
+  ASS(arg1.sort().isArrowSort())
+
+  auto [domain, result] = arg1.sort().asPair();
+
+  ASS(domain == arg2.sort())
+
+  TypedTermList t = {::HOL::create::app(domain, result, arg1, arg2), result};
+
+  if constexpr (sizeof...(args) == 0)
+    return t;
+  else
+    return app(t, args...);
+}
 
 class Defs {
   static Defs* _instance;
@@ -51,7 +65,7 @@ class Defs {
   static Defs* instance();
 
   TermList srt, fSrt;
-  TypedTermList a, f, f2, f3, g;
+  TypedTermList a, f, f2, f3, g, h;
 };
 
 TypedTermList x(unsigned idx, std::optional<TermList> sort = std::nullopt);
diff --git a/UnitTests/HOL/tBetaReduction.cpp b/UnitTests/HOL/tHOL_BetaReduction.cpp
similarity index 96%
rename from UnitTests/HOL/tBetaReduction.cpp
rename to UnitTests/HOL/tHOL_BetaReduction.cpp
index 70a164013..a2e4a85f0 100644
--- a/UnitTests/HOL/tBetaReduction.cpp
+++ b/UnitTests/HOL/tHOL_BetaReduction.cpp
@@ -24,7 +24,7 @@ HOL_TEST_FUN(beta_reduction_1) {
   unsigned reds;
   for (const auto term : testTerms) {
     auto reduced = betaNF(
-      toNameless(app(id(), {term, D.srt})), &reds
+      toNameless(app(id(), TypedTermList(term, D.srt))), &reds
     );
 
     ASS_EQ(reds, 1)
@@ -46,7 +46,7 @@ HOL_TEST_FUN(beta_reduction_2) {
     for (const auto term2 : testTerms) {
       auto constFn = lam(x(0), {term1, D.srt});
       auto reduced = betaNF(
-        toNameless(app(constFn, {term2, D.srt})), &reds
+        toNameless(app(constFn, TypedTermList(term2, D.srt))), &reds
       );
 
       ASS_EQ(reds, 1)
diff --git a/UnitTests/HOL/tEtaReduction.cpp b/UnitTests/HOL/tHOL_EtaReduction.cpp
similarity index 82%
rename from UnitTests/HOL/tEtaReduction.cpp
rename to UnitTests/HOL/tHOL_EtaReduction.cpp
index c10476eb9..dfd80554f 100644
--- a/UnitTests/HOL/tEtaReduction.cpp
+++ b/UnitTests/HOL/tHOL_EtaReduction.cpp
@@ -20,21 +20,21 @@ HOL_TEST_FUN(eta_reduction_1) {
   ASS_EQ(D.a, toNameless(D.a))
   ASS_EQ(etaNF(D.a), D.a)
 
-  auto term = toNameless(lam(x(0), app({D.f, x(0)})));
+  auto term = toNameless(lam(x(0), app(D.f, x(0))));
   ASS_EQ(termListToString(term, Options::HPrinting::TPTP),
          "(^[Y0 : srt]: (f @ Y0))")
   ASS_EQ(termListToString(term, Options::HPrinting::RAW),
          "vLAM(srt,srt,vAPP(srt,srt,f,db0(srt)))")
   ASS_EQ(etaNF(term), D.f)
 
-  term = toNameless(lam({x(0), x(1)}, app({D.f2, x(0), x(1)})));
+  term = toNameless(lam({x(0), x(1)}, app(D.f2, x(0), x(1))));
   ASS_EQ(termListToString(term, Options::HPrinting::TPTP),
          "(^[Y0 : srt]: ((^[Y1 : srt]: (f2 @ Y0 @ Y1))))")
   ASS_EQ(termListToString(term, Options::HPrinting::RAW),
          "vLAM(srt,srt > srt,vLAM(srt,srt,vAPP(srt,srt,vAPP(srt,srt > srt,f2,db1(srt)),db0(srt))))")
   ASS_EQ(etaNF(term), D.f2)
 
-  term = toNameless(lam({x(0), x(1), x(2)}, app({D.f3, x(0), x(1), x(2)})));
+  term = toNameless(lam({x(0), x(1), x(2)}, app(D.f3, x(0), x(1), x(2))));
   ASS_EQ(termListToString(term, Options::HPrinting::TPTP),
          "(^[Y0 : srt]: ((^[Y1 : srt]: ((^[Y2 : srt]: (f3 @ Y0 @ Y1 @ Y2))))))")
   ASS_EQ(termListToString(term, Options::HPrinting::RAW),
@@ -43,7 +43,7 @@ HOL_TEST_FUN(eta_reduction_1) {
 }
 
 HOL_TEST_FUN(eta_reduction_2) {
-  auto term = toNameless(lam({x(0), x(1), x(2)}, app({D.f3, x(0), x(2), x(1)})));
+  auto term = toNameless(lam({x(0), x(1), x(2)}, app(D.f3, x(0), x(2), x(1))));
 
   ASS_EQ(termListToString(term, Options::HPrinting::RAW),
          "vLAM(srt,srt > (srt > srt),vLAM(srt,srt > srt,vLAM(srt,srt,vAPP(srt,srt,vAPP(srt,srt > srt,vAPP(srt,srt > (srt > srt),f3,db2(srt)),db0(srt)),db1(srt)))))");
@@ -51,8 +51,8 @@ HOL_TEST_FUN(eta_reduction_2) {
 }
 
 HOL_TEST_FUN(eta_reduction_3) {
-  auto v0 = x(0, AtomicSort::arrowSort(D.srt, D.srt, D.srt));
-  auto term = toNameless(lam({v0, x(1), x(2)}, app({v0, x(1), x(2)})));
+  auto v0 = x(0, AtomicSort::arrowSort({D.srt, D.srt, D.srt}));
+  auto term = toNameless(lam({v0, x(1), x(2)}, app(v0, x(1), x(2))));
   auto expected = toNameless(lam(v0, v0));
 
   ASS_EQ(expected, HOL::create::namelessLambda(v0.sort(), v0.sort(), HOL::getDeBruijnIndex(0, v0.sort())))
@@ -60,7 +60,7 @@ HOL_TEST_FUN(eta_reduction_3) {
 }
 
 HOL_TEST_FUN(eta_reduction_4) {
-  auto term = toNameless(lam(x(0), app({D.f2, x(0), x(0)})));
+  auto term = toNameless(lam(x(0), app(D.f2, x(0), x(0))));
 
   ASS_EQ(etaNF(term), term)
 }
diff --git a/UnitTests/HOL/tHOL_Printing.cpp b/UnitTests/HOL/tHOL_Printing.cpp
index c3821bcf6..4118485a3 100644
--- a/UnitTests/HOL/tHOL_Printing.cpp
+++ b/UnitTests/HOL/tHOL_Printing.cpp
@@ -118,3 +118,26 @@ HOL_TEST_FUN(hol_print_2) {
       {TPTP,       "(^[Y0 : srt > srt]: ((^[Y1 : srt]: (Y1))))" }}
   );
 }
+
+HOL_TEST_FUN(hol_print_3) {
+  runTest(
+    D.f3.sort(),
+    { {RAW,    "(srt > (srt > (srt > srt)))" },
+      {PRETTY, "(srt → srt → srt → srt)" },
+      {TPTP,   "(srt > srt > srt > srt)"} }
+  );
+
+  runTest(
+    D.g.sort(),
+    { {RAW,    "((srt > srt) > srt)" },
+      {PRETTY, "((srt → srt) → srt)" },
+      {TPTP,   "((srt > srt) > srt)"} }
+  );
+
+  runTest(
+    D.h.sort(),
+    { {RAW,    "((srt > srt) > (srt > srt))" },
+      {PRETTY, "((srt → srt) → srt → srt)" },
+      {TPTP,   "((srt > srt) > srt > srt)"} }
+  );
+}
\ No newline at end of file
diff --git a/UnitTests/HOL/tSubtermReplacer.cpp b/UnitTests/HOL/tHOL_SubtermReplacer.cpp
similarity index 100%
rename from UnitTests/HOL/tSubtermReplacer.cpp
rename to UnitTests/HOL/tHOL_SubtermReplacer.cpp
diff --git a/UnitTests/HOL/tTermShifter.cpp b/UnitTests/HOL/tHOL_TermShifter.cpp
similarity index 100%
rename from UnitTests/HOL/tTermShifter.cpp
rename to UnitTests/HOL/tHOL_TermShifter.cpp
diff --git a/UnitTests/HOL/tHOL_ToPlaceholders.cpp b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
new file mode 100644
index 000000000..0b2567fde
--- /dev/null
+++ b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
@@ -0,0 +1,55 @@
+/*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+
+#include "Kernel/HOL/HOL.hpp"
+#include "Kernel/HOL/ToPlaceholders.hpp"
+#include "Test/HOLUtils.hpp"
+#include "Test/UnitTesting.hpp"
+
+using namespace Test::HOL;
+
+TypedTermList ph(TermList sort) {
+  return {HOL::create::placeholder(sort), sort};
+}
+
+HOL_TEST_FUN(to_placeholders_1) {
+  auto term = app(D.h, D.f, app(x(1, D.fSrt), x(2)));
+  ASS_EQ(term.sort(), D.srt)
+
+  ASS_EQ(
+    termListToString(term, Options::HPrinting::TPTP),
+    "(h @ f @ (X1 @ X2))"
+  )
+
+  ASS_EQ(
+    termListToString(term, Options::HPrinting::RAW),
+    "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,f),vAPP(srt,srt,X1,X2))"
+  )
+
+  auto res = ToPlaceholders::replace(term);
+  ASS_EQ(res, app(D.h, ph(D.fSrt), ph(D.srt)))
+  ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ ph0⟨srt > srt⟩ @ ph0⟨srt⟩)")
+  ASS_EQ(termListToString(res, Options::HPrinting::RAW), "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,ph0(srt > srt)),ph0(srt))")
+
+  // With the setting FunctionExtensionality::OFF, the result of toPlaceholders(h @ f @ (x1 @ x2))
+  // is h @ f @ ☐ as the functional subterm f is not replaced by a placeholder.
+  res = ToPlaceholders::replace(term, Options::FunctionExtensionality::OFF);
+  ASS_EQ(res, app(D.h, D.f, ph(D.srt)))
+  ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ f @ ph0⟨srt⟩)")
+  ASS_EQ(termListToString(res, Options::HPrinting::RAW), "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,f),ph0(srt))")
+}
+
+HOL_TEST_FUN(to_placeholders_2) {
+  const auto res = ToPlaceholders::replace(app(D.h, LAM(D.srt, db(0)), D.a));
+
+  ASS_EQ(res, app(D.h, ph(D.fSrt), D.a))
+  ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ ph0⟨srt > srt⟩ @ a)")
+  ASS_EQ(termListToString(res, Options::HPrinting::RAW), "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,ph0(srt > srt)),a)")
+}
diff --git a/cmake/sources.cmake b/cmake/sources.cmake
index 5fb082254..640e33c19 100644
--- a/cmake/sources.cmake
+++ b/cmake/sources.cmake
@@ -84,10 +84,11 @@ set(UNIT_TESTS
     UnitTests/tTimeTrace.cpp
     UnitTests/tUnificationWithAbstraction.cpp
     UnitTests/HOL/tHOL_Printing.cpp
-    UnitTests/HOL/tBetaReduction.cpp
-    UnitTests/HOL/tEtaReduction.cpp
-    UnitTests/HOL/tTermShifter.cpp
-    UnitTests/HOL/tSubtermReplacer.cpp
+    UnitTests/HOL/tHOL_BetaReduction.cpp
+    UnitTests/HOL/tHOL_EtaReduction.cpp
+    UnitTests/HOL/tHOL_TermShifter.cpp
+    UnitTests/HOL/tHOL_SubtermReplacer.cpp
+    UnitTests/HOL/tHOL_ToPlaceholders.cpp
 )
 
 ################################################################
@@ -462,6 +463,8 @@ set(SOURCES
     Kernel/HOL/EtaNormaliser.hpp
     Kernel/HOL/SubtermReplacer.cpp
     Kernel/HOL/SubtermReplacer.hpp
+    Kernel/HOL/ToPlaceholders.cpp
+    Kernel/HOL/ToPlaceholders.hpp
     Lib/Allocator.cpp
     Lib/Allocator.hpp
     Lib/Array.hpp