Formula
Unify
Sequent
Rules
Instances
Ground
G_ground