pub fn emit_cc(goal: &Syn) -> Option<CcCert>Expand description
Search for a congruence proof of goal — UNTRUSTED.
Saturation over PAIRS rather than a union-find: seed with reflexivity on every subterm of
the goal and with each hypothesis, then close under symmetry, transitivity and congruence,
recording the rule that derived each new pair, until the conclusion appears. The trace is
already in dependency order, because a pair is only ever derived from pairs already in the
list — which is exactly what check_cc demands of the indices.
Congruence is applied only where the LEFT side already occurs in the goal’s term table.
Without that restriction the saturation is unbounded — f x can always be applied again —
and an emitter that does not terminate is a re-checker that hangs.