Repository navigation
Strengthen the formal result to show that p -> p is not a substitution instance of any member of the condensed-detachment closure. Add and verify substitution-weight monotonicity, replace three incidental native_decide base cases with kernel-checked proofs, align theorem comments with the JAR sequel manuscript, and correct the README.