Logical variables
A new extension of Prop involve the extension of logical variables.
With the introduction of logical variables, tree structures
formed from algebraic datatypes become Herbrand terms, pattern matching
becomes unification, and rewriting becomes narrowing.
Constraints
Feature trees