pub fn simplify_trivial_identities(premises: &[ProofExpr]) -> Vec<ProofExpr>Expand description
Fold away trivial (reflexive) identities and the boolean constants they create: a
grounded ∃x∃y of-pair has a DIAGONAL instance (x = y = c) carrying ¬(c = c),
which is False, so that disjunct must drop. Without it the solver would face an
unsatisfiable disjunct it cannot refute (the kernel has no reflexivity rule to prove
c = c). Identity(c,c) ↦ True, ¬True ↦ False, then ∧/∨/→ constant-fold.