Coherent formula
= Coherent formula
A coherent formula is built from atomic relations and equality using $\top$, $\bot$, finite conjunction, finite disjunction and existential quantification. General negation and universal quantification are not constructors. Substitution of well-typed terms preserves coherent formulas.