for the collection of formulae attached to the universe-of-discourse, provide support for standard formulae
use this new feature to simplify the verification of standard parameters (e.g. p_implies_q, q_implies_q, etc.)
question: when we have an inference-rule with multiple premises (e.g. p_implies_q and q_implies_p), it would be more natural to group them together in a single formula with the sequent-comma operator. but then, to facilitate the composition of more complex formula from building blocks, we could provide a new formula construction function that creates a new formula from others but intelligently rescope variables?
question: when we have an inference-rule with multiple premises (e.g. p_implies_q and q_implies_p), it would be more natural to group them together in a single formula with the sequent-comma operator. but then, to facilitate the composition of more complex formula from building blocks, we could provide a new formula construction function that creates a new formula from others but intelligently rescope variables?