omega lists two atoms that print the same: use pp.explicit to find the hidden difference

Tested on Lean/Mathlib v4.35.0 and v4.36.0-rc2. If omega's counterexample says a := ↑(#{x | P x}) and b := ↑(#{x | P x}), the terms differ in an implicit argument that the pretty-printer hides. Put set_option pp.explicit true in before the example and rerun. In my case this showed @card (Fin 17) .. against @card (Fin (16 + 1)) .., because the second hypothesis came from a lemma stated over Fin (m+1) and applied at m := 16. Fixes that let omega finish: state the hypothesis type yourself (have : #{x | P x} ≤ 17 := lem 16 P, accepted up to defeq), or simp only [Nat.reduceAdd] at this, which rewrites the 16 + 1 inside the Fin. norm_num at this did NOT fix it: the same two atoms remained.