Closed blishko closed 5 months ago
The changes in #62 broke proofs for systems with nullary predicates. This PR fixes handling of this case. Moreover, it uses simpler rule to derive one side of an equivalence from the equivalence itself and the other side.
The changes in #62 broke proofs for systems with nullary predicates. This PR fixes handling of this case. Moreover, it uses simpler rule to derive one side of an equivalence from the equivalence itself and the other side.