Commit 2023-05-17 23:46 de0cf0af

fix: use cleanupAnnotations in symm and trans (#3768)

• trans would fail if the goal had an annotation
• symm would use whnf with normal transparency on the goal, now we use cleanupAnnotations.
• rfl is fixed in #3758