Function check_cc 

pub fn check_cc(goal: &Syn, cert: &CcCert) -> bool

Check a congruence proof against a goal.

A LINEAR REPLAY: each step’s conclusion is computed from steps that come strictly BEFORE it, each premise is checked to say what its rule needs it to say, and the last step must be the goal’s conclusion, orientation included. There is no union-find here and no e-graph; a checker that rebuilt one would be the copy this module exists to avoid.