pub fn at_most_one_lemmas(premises: &[ProofExpr]) -> Vec<ProofExpr>Expand description
“Exactly one φ” entails “at most one φ” — for every premise of the form
∃x(φ(x) ∧ ∀y(φ(y) → y = x)) (what Cardinal(1) produces), emit the PAIRWISE
uniqueness ∀x∀y((φ(x) ∧ φ(y)) → x = y).
Why: the existence form grounds to a DISJUNCTION whose disjuncts nest the
uniqueness rule, which the certified backward-chainer cannot use directly; the
pairwise form grounds to plain conjunctive implications it discharges by forward
chaining (the shape grounded_two_value_grid_proves_with_our_kernel proves). The
lemma is logically ENTAILED by the original, so adding it is sound, and it is
GENERAL over any “exactly one” statement — never tied to a particular puzzle.