From Undecidability.FOL.Syntax Require Export Core Subst Bounded DiscreteEnumerable SyntacticOps.