requirement: the variable-substitution inference-rule must forbid the substitution of strictly-propositional objects with non-strictly-propositional objects

[daviddoret]

variable-substitution must forbid the substitution of propositional objects with non-(strictly)-propositional objects. in effect, this would allow the inference of ill-defined formula in the theory-elaboration-sequence.

implementation:

• [ ] in the variable-substitution inference-rule inclusion, in the check_premises_validity() method, check that this requirement is complied with. if not, raise an exception.
• [ ] in the variable-substitution inference-rule declaration, in the construct_formula() method, check that this requirement is complied with. if not, raise a warning? alternatively, let configuration define if this should raise an exception.

documentation:

• [ ] align the documentation of the is_propositional property on all applicable classes, making cross-references between the documentation of the property and the documentation of the inference-rule.